Fermat's Last Theorem in Lean 4

Namespace `FixedPart` 3 theorems

Common kernel vector with zero annihilator for a square-zero family FixedPart.exists_smul_eq_zero_forall_of_comp_eq_zero 0 below · cited by 1 · depth 23
Nondegenerate trace pairing on a reduced ℤ-order FixedPart.exists_trace_mul_ne_zero 0 below · cited by 1 · depth 23
Reducedness and Artinianity of a ℚ_q-algebra spanned by an order with nondegenerate trace FixedPart.isReduced_of_linearIndependent_of_trace 0 below · cited by 1 · depth 23

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.