Fermat's Last Theorem in Lean 4

Namespace `RatIdele` 2 theorems

Absolute value of an idele class character of ℚ RatIdele.exists_norm_apply_eq_ideleNorm_rpow 5 below · cited by 7 · depth 15
Everywhere-unit finite idele congruent to its residue mod M RatIdele.sub_natCast_val_unitResidue_mem_idealBall_of_forall_valued_eq_one 0 below · cited by 1 · depth 18

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.