Fermat's Last Theorem in Lean 4

Namespace `KummerO` 5 theorems

Block idempotents for points with inertia-trivial quotient KummerO.exists_blockIdempotents_of_quotient_inertiaTrivial 20 below · cited by 1 · depth 13
Kummer generators for one block of a finite free Hopf algebra KummerO.exists_units_of_block 12 below · cited by 1 · depth 13
Unit-Kummer generators trivialising inertia on Hopf algebra points KummerO.forall_eq_of_finiteFreeHopf_of_inertiaCyclotomic_of_quotient_inertiaTrivial_of_isAlgClosed 23 below · cited by 1 · depth 18
Block idempotents indexed by cosets of a cyclotomic submonoid of points KummerO.exists_blockIdempotents_of_quotient_inertiaTrivial_of_isAlgClosed 19 below · cited by 1 · depth 19
Kummer units for a block of q-torsion Hopf algebra points KummerO.exists_units_of_block_of_isAlgClosed 12 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.