Commit 2026-06-23 10:39 10874878

View on Github →

chore(RingTheory/Invariant/Basic): split file by imports (#40928) The basic file RingTheory/Invariant/Basic.lean proving existence of Frobenius elements has surprisingly heavy imports (e.g., all of Galois theory). This PR splits off the heaver material into a separate file RingTheory/Invariant/Galois.lean. This leads to some nontrivial import reductions in downstream files.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/NumberTheory/RamificationInertia/Galois.lean

Modified Mathlib/RingTheory/Invariant/Basic.lean

deleted theorem Algebra.isInvariant_of_isGalois'

deleted theorem Algebra.isInvariant_of_isGalois

deleted theorem Ideal.IsFractionRing.finite_of_isInvariant

deleted theorem Ideal.IsFractionRing.normal

deleted theorem Ideal.Quotient.finite_of_isInvariant

deleted theorem Ideal.Quotient.normal

Created Mathlib/RingTheory/Invariant/Galois.lean

added theorem Algebra.isInvariant_of_isGalois'

added theorem Algebra.isInvariant_of_isGalois

added theorem Ideal.IsFractionRing.finite_of_isInvariant

added theorem Ideal.IsFractionRing.normal

added theorem Ideal.Quotient.finite_of_isInvariant

added theorem Ideal.Quotient.normal