iff_isSeparable — Mathlib

English

Under EssFiniteType K L, FormallyEtale K L is equivalent to Algebra.IsSeparable K L.

Русский

При EssFiniteType K L формально étale эквивалентно Algebra.IsSeparable K L.

LaTeX

$$$[EssFiniteType K L] : \text{FormallyEtale } K L \iff \text{Algebra.IsSeparable } K L$$$

Lean4

theorem iff_isSeparable [EssFiniteType K L] : FormallyEtale K L ↔ Algebra.IsSeparable K L :=
  ⟨fun _ ↦ FormallyUnramified.isSeparable K L, fun _ ↦ of_isSeparable K L⟩

Похожие утверждения