English
If k is a field, k is algebraically closed, and K is a ring, then any polynomial p over K splits in the codomain via f: K →+* k.
Русский
Пусть k — поле, k алгебраически замкнуто, K — кольцо. Любой многочлен p над K распадается в кодом K через f: K →+* k.
LaTeX
$$$p.Splits\, f$ under $[\text{Field } k], [\IsAlgClosed k], [\CommRing K]$ with $f: K \to k$.$$
Lean4
/-- Every polynomial splits in the field extension `f : K →+* k` if `k` is algebraically closed.
See also `IsAlgClosed.splits_domain` for the case where `K` is algebraically closed.
-/
theorem splits_codomain {k K : Type*} [Field k] [IsAlgClosed k] [CommRing K] {f : K →+* k} (p : K[X]) : p.Splits f := by
convert IsAlgClosed.splits (p.map f); simp [splits_map_iff]
