Theorem Algebra.FormallyEtale.of_isSeparable

Modification history

2024-10-26 13:47
Mathlib/RingTheory/Etale/Field.lean
feat(RingTheory/Etale): etale <=> separable for field extensions of finite type. (#17633)
Added Algebra.FormallyEtale.of_isSeparableView on Github →