Theorem Ideal.IsDedekindDomain.ramificationIdx_eq_one_iff

Modification history

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