Theorem Ideal.ramificationIdx_eq_one_of_map_localization

Modification history

2026-03-25 22:20
Mathlib/NumberTheory/RamificationInertia/Basic.lean
chore(NumberTheory/RamificationInerta/Basic): split file (#37173) …
Modified Ideal.ramificationIdx_eq_one_of_map_localizationView on Github →
2025-06-07 07:26
Mathlib/NumberTheory/RamificationInertia/Basic.lean
feat: connection between `Algebra.IsUnramifiedAt` and `Ideal.ramificationIdx`. (#25498)
Added Ideal.ramificationIdx_eq_one_of_map_localizationView on Github →