Theorem IsLocalization.AtPrime.inertiaDeg_map_eq_inertiaDeg

Modification history

2026-01-11 14:20
Mathlib/RingTheory/Localization/AtPrime/Extension.lean
feat(RingTheory/Localization/AtPrime): inertia degree and ramification index are preserved by localization (#27706) …
Added IsLocalization.AtPrime.inertiaDeg_map_eq_inertiaDegView on Github →