Fermat's Last Theorem in Lean 4

Namespace `M4aKummer` 5 theorems

Norm-class index divides |Gal(E/k)| in 2-power degree M4aKummer.normClassIndex_dvd_card_aut 67 below · cited by 3 · depth 15
Second inequality for solvable Galois extensions M4aKummer.normClassIndex_dvd_card_aut_of_isSolvable 104 below · cited by 3 · depth 15
Second inequality in norm-class form, prime-power Galois degree M4aKummer.normClassIndex_dvd_card_aut_of_prime_pow 103 below · cited by 1 · depth 16
Tower divisibility for narrow ray norm-class indices M4aKummer.normClassIndex_dvd_mul_of_tower 0 below · cited by 3 · depth 16
Second inequality for quadratic extensions: index divides 2 M4aKummer.normClassIndex_dvd_two 65 below · cited by 1 · depth 16

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.