Commit 2026-06-15 13:16 ddd592eb

View on Github →

feat(RingTheory/Invariant/Basic): generalize Ideal.Quotient.normal to IsFractionRing (#40247) This PR generalizes Ideal.Quotient.normal to IsFractionRing (currently it only holds for quotients of maximal ideals). I have left both versions since that is the pattern of the file (to have both an IsFractionRing version and an Ideal.Quotient version).

Estimated changes

Modified Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean

Modified Mathlib/RingTheory/Invariant/Basic.lean

added theorem Ideal.IsFractionRing.finite_of_isInvariant

added theorem Ideal.IsFractionRing.normal

added theorem MulSemiringAction.splits_charpoly

Modified Mathlib/RingTheory/Localization/Integral.lean

modified theorem isAlgebraic_of_isFractionRing