Fermat's Last Theorem in Lean 4

Namespace `BrauerNesbitt` 2 theorems

Brauer–Nesbitt: equal traces and spanning image give isomorphism BrauerNesbitt.exists_linearEquiv_of_span_range_eq_top_of_trace_eq 0 below · cited by 5 · depth 10
Brauer–Nesbitt: irreducibles with equal traces are isomorphic BrauerNesbitt.case_irreducible_irreducible 0 below · cited by 1 · depth 22

Documents the Lean sources in this repository (Lean v4.33.1, Mathlib v4.33.0). Statements are quoted textually from the .lean files; dependency edges are the import Theorems.Thm_… lines of the proof modules. About these pages.