Theorem IsLocalization.AtPrime.ramificationIdx_map_eq_ramificationIdx

Modification history

2026-06-30 10:21
Mathlib/RingTheory/Localization/AtPrime/Extension.lean
refactor(RingTheory/Localization/AtPrime/Extension): switch to new definition of ramification index (#40781) …
Modified IsLocalization.AtPrime.ramificationIdx_map_eq_ramificationIdxView on Github →
2026-01-13 19:40
Mathlib/RingTheory/Localization/AtPrime/Extension.lean
chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree` wlog (#30563) …
Modified IsLocalization.AtPrime.ramificationIdx_map_eq_ramificationIdxView on Github →
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.ramificationIdx_map_eq_ramificationIdxView on Github →