English
If f ∈ K[X] splits over id and is monic, and every root lies in the range of algebraMap, then f lies in Polynomial.lifts (algebraMap R K).
Русский
Если f ∈ K[X] распадается над идентичным отображением и моничный, и каждый корень лежит в диапазоне algebraMap, тогда f принадлежит Polynomial.lifts (algebraMap R K).
LaTeX
$$$\\forall R,K,L,\\; [Algebra R K] \,[Algebra R L]\\; {f : K[X]}\\; (\\text{Splits}(\\mathrm{algebraMap } R K,f)) \\land f.Monic \\land (\\forall a \\in f.\\text{roots}, a \\in (\\mathrm{algebraMap } R K).range) \\Rightarrow f \\in Polynomial.lifts(\\mathrm{algebraMap } R K).$$$
Lean4
theorem eq_X_sub_C_of_splits_of_single_root {x : K} {h : K[X]} (h_splits : Splits i h)
(h_roots : (h.map i).roots = {i x}) : h = C h.leadingCoeff * (X - C x) :=
by
apply Polynomial.map_injective _ i.injective
rw [eq_prod_roots_of_splits h_splits, h_roots]
simp
