Fermat's Last Theorem in Lean 4

Namespace `MazurRapoportAppendix` 2 theorems

Degree-zero sublattice transports along multiplicity-preserving bijections MazurRapoportAppendix.SpecialFibreComponentTable.mem_degreeZeroSublattice_iff_comp_of_mult_equiv 0 below · cited by 1 · depth 16
Transport of imα along an intersection-preserving reindexing MazurRapoportAppendix.SpecialFibreComponentTable.mem_range_intersectionAlpha_iff_comp_of_inter_equiv 0 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.