Fermat's Last Theorem in Lean 4

Namespace `FinFlatHopf` 5 theorems

Inertia acts multiplicatively on a subgroup with unramified quotient FinFlatHopf.exists_subgroup_inertia_trivial_quotient_cyclotomic 10 below · cited by 1 · depth 14
Points of the Cartier dual as characters of the points FinFlatHopf.dualPoints_equiv_monoidHom 0 below · cited by 7 · depth 15
Inertia-fixed subring of a place over p: uniformiser p FinFlatHopf.inertiaFixed_valuationSubring_dvr_fixer_le_inertia 3 below · cited by 2 · depth 15
Local Hopf algebra of rank n has non-local convolution dual FinFlatHopf.not_isLocalRing_dual_of_isLocalRing 1 below · cited by 1 · depth 15
Left integral and Frobenius map over a local base FinFlatHopf.exists_left_integral_frobenius 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.