Theorem Algebra.FormallyEtale.iff_of_equiv

Modification history

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