Theorem Ideal.ramificationIdx_map_self_eq_one

Modification history

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