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