2026-02-13 12:37
Mathlib/RingTheory/Invariant/Basic.lean
feat(RingTheory/Ideal): isomorphism between `stabilizer G Q / inertia G Q` and the Galois group of the residue fields extension (#34730) …
Added Ideal.Quotient.stabilizerQuotientInertiaEquiv_mk