Theorem Algebra.IsUnramifiedAt.of_liesOver

Modification history

2025-06-07 07:26

Mathlib/NumberTheory/RamificationInertia/Unramified.lean

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

Added Algebra.IsUnramifiedAt.of_liesOver View on Github →