Theorem Ideal.Quotient.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.Quotient.finite_of_isInvariantView on Github →
2025-09-27 10:51
Mathlib/RingTheory/Invariant/Basic.lean
feat(RingTheory/Invariant): residue field extension is finite (#25616)
Added Ideal.Quotient.finite_of_isInvariantView on Github →