perfectField — Mathlib

English

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

Русский

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

LaTeX

$$$\text{ PerfectField } L$ (при \(L/K\text{ алгебраическое и } K\text{ совершенное})$$$

Lean4

/-- If `L / K` is an algebraic extension, `K` is a perfect field, then so is `L`. -/
theorem perfectField {K L : Type*} [Field K] [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [PerfectField K] :
    PerfectField L :=
  ⟨fun {f} hf ↦ by
    obtain ⟨_, _, hi, h⟩ := hf.exists_dvd_monic_irreducible_of_isIntegral (K := K)
    exact (PerfectField.separable_of_irreducible hi).map |>.of_dvd h⟩

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