iff_isSeparable — Mathlib

English

For FormallyUnramified K L with EssFiniteType K L, FormallyUnramified K L is equivalent to Algebra.IsSeparable K L.

Русский

При FormallyUnramified K L с EssFiniteType K L формально неразветвленность эквивалентна сепарабельности над K.

LaTeX

$$$[\text{FormallyUnramified } K L] \iff [\text{IsSeparable } K L]$$$

Lean4

theorem iff_isSeparable (L : Type u) [Field L] [Algebra K L] [EssFiniteType K L] :
    FormallyUnramified K L ↔ Algebra.IsSeparable K L :=
  ⟨fun _ ↦ isSeparable K L, fun _ ↦ of_isSeparable K L⟩

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