Theorem Ideal.ramificationIdx_eq_one_of_isUnramifiedAt

Modification history

2025-06-07 07:26
Mathlib/NumberTheory/RamificationInertia/Unramified.lean
feat: connection between `Algebra.IsUnramifiedAt` and `Ideal.ramificationIdx`. (#25498)
Added Ideal.ramificationIdx_eq_one_of_isUnramifiedAtView on Github →