Theorem Algebra.FormallyUnramified.isReduced_of_field

Modification history

2024-10-03 17:34

Mathlib/RingTheory/Unramified/Field.lean

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

Added Algebra.FormallyUnramified.isReduced_of_field View on Github →