isSeparable_of_perfectField — Mathlib

English

If L/K is algebraic and K is a perfect field, then L/K is separable.

Русский

Если расширение L/K алгебраическое и K — совершенное поле, то расширение L/K расслоимо.

LaTeX

$$$\text{ Algebra.IsSeparable } K L$ (при условии PerfectField K) $$$

Lean4

/-- If `L / K` is an algebraic extension, `K` is a perfect field, then `L / K` is separable. -/
instance isSeparable_of_perfectField {K L : Type*} [Field K] [Field L] [Algebra K L] [Algebra.IsAlgebraic K L]
    [PerfectField K] : Algebra.IsSeparable K L :=
  ⟨fun x ↦ PerfectField.separable_of_irreducible <| minpoly.irreducible (Algebra.IsIntegral.isIntegral x)⟩

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