Theorem IsUnramifiedAt.of_liesOver_of_ne_bot

Modification history

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