splits_domain — Mathlib

English

If k is separably closed, then every separable polynomial over k splits in K via f.

Русский

Если k является сепарабельным замкнутым полем, то каждый сепарабельный многочлен над k раскладывается в расширении над k через f.

LaTeX

$$$p.Separable \Rightarrow p.Splits f$$$

Lean4

/-- Every separable polynomial splits in the field extension `f : k →+* K` if `k` is
separably closed.

See also `IsSepClosed.splits_codomain` for the case where `k` is separably closed.
-/
theorem splits_domain [IsSepClosed k] {f : k →+* K} (p : k[X]) (h : p.Separable) : p.Splits f :=
  Polynomial.splits_of_splits_id _ <| IsSepClosed.splits_of_separable _ h

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