Theorem Algebra.FormallyUnramified.of_isSeparable

Modification history

2024-10-03 17:34

Mathlib/RingTheory/Unramified/Field.lean

feat(RingTheory/Unramified): Classification of unramifield field extensions. (#15123)

Added Algebra.FormallyUnramified.of_isSeparable View on Github →