Fermat's Last Theorem in Lean 4

Namespace `IsNonarchimedean` 3 theorems

Unit coordinates are preserved by small Plücker minors IsNonarchimedean.abv_apply_eq_one_of_iSup_abv_mul_sub_mul_lt_one 0 below · cited by 3 · depth 19
Elements integral over ℤ have non-archimedean absolute value ≤ 1 IsNonarchimedean.apply_le_one_of_isIntegral_int 0 below · cited by 1 · depth 19
Ultrametric 2× 2 minors at a common pivot IsNonarchimedean.iSup_abv_mul_sub_mul_eq_iSup_abv_sub 0 below · cited by 1 · depth 19

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.