Theorem Ideal.Quotient.normal

Modification history

2025-09-27 10:51

Mathlib/RingTheory/Invariant/Basic.lean

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

Added Ideal.Quotient.normal View on Github →