Theorem Ideal.Quotient.ker_stabilizerHom

Modification history

2026-06-04 13:23
Mathlib/RingTheory/Ideal/Over.lean
feat(RingTheory/Invariant/Basic): add isomorphism version of `IsFractionRing.stabilizerHom` (#40203) …
Modified Ideal.Quotient.ker_stabilizerHomView on Github →
2025-10-26 15:49
Mathlib/RingTheory/Ideal/Over.lean
feat(NumberTheory): order of inertia group = ramification index (#30675)
Added Ideal.Quotient.ker_stabilizerHomView on Github →