roots_prod — Mathlib

English

From a list of polynomials with nonzero product, the roots of the product equal the bind of the roots of the list elements.

Русский

Из списка полиномов с непустым произведением следует, что корни произведения равны объединению корней элементов списка.

LaTeX

$$$ \forall f:\,\text{List}(R[X]), \prod f \neq 0 \Rightarrow (\prod f).roots = (f).bind roots $$$

Lean4

theorem roots_prod {ι : Type*} (f : ι → R[X]) (s : Finset ι) :
    s.prod f ≠ 0 → (s.prod f).roots = s.val.bind fun i => roots (f i) :=
  by
  rcases s with ⟨m, hm⟩
  simpa [Multiset.prod_eq_zero_iff, Multiset.bind_map] using roots_multiset_prod (m.map f)

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