English
If k is algebraically closed and K is a field, then any polynomial p over k splits in the domain via a map, i.e., the splits property holds on the domain side as well.
Русский
Пусть k алгебраически замкнутое, K — поле. Любой многочлен над k распадается в доменном отображении.
LaTeX
$$$p.Splits\, f$ where $f: k \to K$ and $[\IsAlgClosed k], [\Field K]$.$$
Lean4
/-- Every polynomial splits in the field extension `f : K →+* k` if `K` is algebraically closed.
See also `IsAlgClosed.splits_codomain` for the case where `k` is algebraically closed.
-/
theorem splits_domain {k K : Type*} [Field k] [IsAlgClosed k] [Field K] {f : k →+* K} (p : k[X]) : p.Splits f :=
Polynomial.splits_of_splits_id _ <| IsAlgClosed.splits _
