Theorem Ideal.card_stabilizer_eq

Modification history

2026-06-18 11:44
Mathlib/NumberTheory/RamificationInertia/Galois.lean
feat(NumberTheory/RamificationInertia/Galois): ramification inertia refactor (#40126) …
Modified Ideal.card_stabilizer_eqView on Github →
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_eqView on Github →