English
Let k and K be fields and f: k →+* K a field hom. If K is separably closed and p ∈ k[X] is separable, then p splits completely in K via f.
Русский
Пусть k и K — поля, f: k →+* K гомоморфизм полей. Если K является сепарабельным замкнутым полем и p ∈ k[X] сепарабельный, то p раскладывается полностью над 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_domain` for the case where `k` is separably closed.
-/
theorem splits_codomain [IsSepClosed K] {f : k →+* K} (p : k[X]) (h : p.Separable) : p.Splits f := by
convert IsSepClosed.splits_of_separable (p.map f) (Separable.map h); simp [splits_map_iff]
