prod_multiset_root_eq_finset_root

English

For any nonzero polynomial p, the product ∏ a∈p.roots (X − a) divides p when counted with multiplicities, in a suitable sense.

Русский

Для любой ненулевого многочлена p произведение по корням ∏ a∈p.roots (X − a) делит p с учётом кратностей.

LaTeX

$$(p.roots.map (λ a, X − C a)).prod ∣ p$$

Lean4

theorem prod_multiset_root_eq_finset_root [DecidableEq R] :
    (p.roots.map fun a => X - C a).prod = p.roots.toFinset.prod fun a => (X - C a) ^ rootMultiplicity a p := by
  simp only [count_roots, Finset.prod_multiset_map_count]

Похожие утверждения