English
For a polynomial p, there exists q such that (X − a1)···(X − ak) · q = p, with q having no roots and deg relations between root count and p.
Русский
Для многочлена p существует q, что произведение по корням умножается на q и даёт p, причём q имеет нулевые корни и соблюдается отношение степеней.
LaTeX
$$∃ q, (p.roots.map (λ a, X − C a)).prod · q = p ∧ p.roots.card + q.natDegree = p.natDegree ∧ q.roots = 0$$
Lean4
theorem exists_prod_multiset_X_sub_C_mul (p : R[X]) :
∃ q,
(p.roots.map fun a => X - C a).prod * q = p ∧ Multiset.card p.roots + q.natDegree = p.natDegree ∧ q.roots = 0 :=
by
obtain ⟨q, he⟩ := p.prod_multiset_X_sub_C_dvd
use q, he.symm
obtain rfl | hq := eq_or_ne q 0
· rw [mul_zero] at he
subst he
simp
constructor
· conv_rhs => rw [he]
rw [(monic_multisetProd_X_sub_C p.roots).natDegree_mul' hq, natDegree_multiset_prod_X_sub_C_eq_card]
· replace he := congr_arg roots he.symm
rw [roots_mul, roots_multiset_prod_X_sub_C] at he
exacts [add_eq_left.1 he, mul_ne_zero (monic_multisetProd_X_sub_C p.roots).ne_zero hq]
