Commit 2024-10-26 13:47 e2338ffc

View on Github →

feat(RingTheory/Etale): etale <=> separable for field extensions of finite type. (#17633)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/Etale/Basic.lean

added theorem Algebra.FormallyEtale.iff_of_equiv

Created Mathlib/RingTheory/Etale/Field.lean

added theorem Algebra.FormallyEtale.iff_isSeparable

added theorem Algebra.FormallyEtale.of_isSeparable

added theorem Algebra.FormallyEtale.of_isSeparable_aux

Modified Mathlib/RingTheory/Smooth/Basic.lean

added theorem Algebra.FormallySmooth.iff_of_equiv

Modified Mathlib/RingTheory/Unramified/Basic.lean

added theorem Algebra.FormallyUnramified.iff_of_equiv