Commit 2024-10-03 17:34 6b2a1227

View on Github →

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

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Polynomial/Taylor.lean

added theorem Polynomial.eval_add_of_sq_eq_zero

Created Mathlib/RingTheory/Unramified/Field.lean

added theorem Algebra.FormallyUnramified.bijective_of_isAlgClosed_of_localRing

added theorem Algebra.FormallyUnramified.iff_isSeparable

added theorem Algebra.FormallyUnramified.isField_of_isAlgClosed_of_localRing

added theorem Algebra.FormallyUnramified.isReduced_of_field

added theorem Algebra.FormallyUnramified.isSeparable

added theorem Algebra.FormallyUnramified.of_isSeparable

added theorem Algebra.FormallyUnramified.range_eq_top_of_isPurelyInseparable