Theorem Ideal.IsFractionRing.finite_of_isInvariant

Modification history

2026-06-23 10:39

Mathlib/RingTheory/Invariant/Basic.lean

chore(RingTheory/Invariant/Basic): split file by imports (#40928) …

Modified Ideal.IsFractionRing.finite_of_isInvariant View on Github →

2026-06-15 13:16

Mathlib/RingTheory/Invariant/Basic.lean

feat(RingTheory/Invariant/Basic): generalize `Ideal.Quotient.normal` to `IsFractionRing` (#40247) …

Added Ideal.IsFractionRing.finite_of_isInvariant View on Github →