Fermat's Last Theorem in Lean 4

Namespace `IsGaloisGroup` 5 theorems

Inertia ring is finite étale with full residue field IsGaloisGroup.exists_subalgebra_fixedPoints_inertia_etale_and_isLocalRing_and_finrank_eq 19 below · cited by 2 · depth 28
Tame invariants: finite presentation, normality, flatness and smoothness descend IsGaloisGroup.finitePresentation_and_smooth_invariants_typeZero_of_isUnit_natCard_of_smooth_fibers 3 below · cited by 15 · depth 29
Degree of the fraction field of H-invariants equals (G:H) IsGaloisGroup.finrank_eq_index_of_isFractionRing_fixedPoints 0 below · cited by 1 · depth 29
Reynolds retraction onto the invariants of a tame group action IsGaloisGroup.exists_retraction_and_forall_ideal_invariants_of_isUnit_natCard 0 below · cited by 1 · depth 30
Invariant subrings of integrally closed domains are integrally closed IsGaloisGroup.isIntegrallyClosed_of_isIntegrallyClosed 0 below · cited by 4 · depth 30

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.