Fermat's Last Theorem in Lean 4

Namespace `RibetLevelLowering` 4 theorems

Toric dichotomy plus no lower-level torsion gives J[𝔪]subseteqT RibetLevelLowering.heckeTorsion_le_toric_of_toricDichotomy 0 below · cited by 2 · depth 10
Character duality in dimension form: T[𝔪] versus L/𝔪 L RibetLevelLowering.finrank_span_torsion_eq_finrank_quotient_of_characterDuality 0 below · cited by 2 · depth 14
Snake-lemma transfer of kernel and cokernel for lattice pairings RibetLevelLowering.gramSnake_ker_and_coker_transfer 0 below · cited by 2 · depth 17
Equal 𝔪-coinvariant counts from Eisenstein kernel and cokernel RibetLevelLowering.natCard_quotient_eq_natCard_quotient_of_eisenstein_ker_of_eisenstein_coker 0 below · cited by 2 · depth 17

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.