English
For any polynomial p, the product of (X − a) over its roots divides p.
Русский
Произведение по корням делит сам многочлен.
LaTeX
$$(p.roots.map (λ a, X − C a)).prod ∣ p$$
Lean4
/-- The product `∏ (X - a)` for `a` inside the multiset `p.roots` divides `p`. -/
theorem prod_multiset_X_sub_C_dvd (p : R[X]) : (p.roots.map fun a => X - C a).prod ∣ p := by
classical
rw [← map_dvd_map _ (IsFractionRing.injective R <| FractionRing R) (monic_multisetProd_X_sub_C p.roots)]
rw [prod_multiset_root_eq_finset_root, Polynomial.map_prod]
refine Finset.prod_dvd_of_coprime (fun a _ b _ h => ?_) fun a _ => ?_
· simp_rw [Polynomial.map_pow, Polynomial.map_sub, map_C, map_X]
exact (pairwise_coprime_X_sub_C (IsFractionRing.injective R <| FractionRing R) h).pow
· exact Polynomial.map_dvd _ (pow_rootMultiplicity_dvd p a)
