Theorem Algebra.isUnramifiedAt_iff_of_isDedekindDomain

Modification history

2025-06-07 07:26

Mathlib/NumberTheory/RamificationInertia/Unramified.lean

feat: connection between `Algebra.IsUnramifiedAt` and `Ideal.ramificationIdx`. (#25498)

Added Algebra.isUnramifiedAt_iff_of_isDedekindDomain View on Github →