Theorem Ideal.sum_ramification_inertia_eq_card

Modification history

2026-06-08 10:43
Mathlib/RingTheory/RamificationInertia/Basic.lean
feat(RingTheory/RamificationInertia/Basic): ramification-inertia formula for finite flat extensions (#39189) …
Added Ideal.sum_ramification_inertia_eq_cardView on Github →