Fermat's Last Theorem in Lean 4

Namespace `QuadraticForm` 5 theorems

Anisotropy of a quaternary norm form versus its ternary subform QuadraticForm.forall_quaternary_normForm_eq_zero_iff_forall_ternary_eq_zero 0 below · cited by 8 · depth 18
Local–global principle for the ternary form -ax²-by²+abz² QuadraticForm.exists_rat_ternary_pureNrd_eq_of_forall_adicCompletion_of_real 0 below · cited by 11 · depth 19
Pure norm form represents c at a non-split place QuadraticForm.exists_ternary_pureNrd_eq_adicCompletion_of_not_isSquare_neg_of_not_split 0 below · cited by 11 · depth 19
Isotropic ternary form -ax²-by²+abz² is universal QuadraticForm.forall_exists_ternary_pureNrd_eq_of_exists_ne_zero_eq_zero 0 below · cited by 11 · depth 19
Multiplicativity of isotropy for z²-tx²-uy² QuadraticForm.exists_ternary_isotropic_mul_of_exists_of_exists 0 below · cited by 1 · depth 30

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.