Theorem Ideal.Quotient.map_ker_stabilizer_subtype

Modification history

2025-10-26 15:49
Mathlib/RingTheory/Ideal/Over.lean
feat(NumberTheory): order of inertia group = ramification index (#30675)
Added Ideal.Quotient.map_ker_stabilizer_subtypeView on Github →