Theorem Algebra.isUnramifiedAt_iff_map_eq

Modification history

2025-02-04 14:13

Mathlib/RingTheory/Unramified/LocalRing.lean

feat(RingTheory): unramified iff `κ(q)/κ(p)` is separable and `pS_q = qS_q` (#20690)

Added Algebra.isUnramifiedAt_iff_map_eq View on Github →