Fermat's Last Theorem in Lean 4

Namespace `FiniteField` 4 theorems

Row-by-row avoidance of affine conditions over a finite field FiniteField.exists_forall_affineMap_apply_ne_zero_of_forall_lt 1 below · cited by 1 · depth 25
Fewer than q affine conditions on 𝔽ⁿ are simultaneously avoidable FiniteField.exists_forall_affineMap_ne_zero 0 below · cited by 1 · depth 26
Finite fields of characteristic p embed into A/pA for A⊆ℂ FiniteField.exists_subring_complex_isMaximal_span_natCast_ringHom 0 below · cited by 1 · depth 26
Finite extensions of equal cardinality are K-isomorphic FiniteField.nonempty_algEquiv_of_card_eq 0 below · cited by 1 · depth 36

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.