Theorem Algebra.FormallyUnramified.iff_of_equiv

Modification history

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