Theorem Ideal.Quotient.finite_of_isInvariant

Modification history

2025-09-27 10:51

Mathlib/RingTheory/Invariant/Basic.lean

feat(RingTheory/Invariant): residue field extension is finite (#25616)

Added Ideal.Quotient.finite_of_isInvariant View on Github →