Theorem Algebra.FormallyEtale.of_isSeparable_aux

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_isSeparable_auxView on Github →