roots_multiset_prod — Mathlib

English

The multiset product version of roots of a family of polynomials.

Русский

Мультимножество произведение корней семейства полиномов.

LaTeX

$$$ \text{Theorem: } m : Multiset (R[X]) \Rightarrow \ Not (m = 0) → m.prod.roots = m.bind (roots) $$$

Lean4

theorem roots_multiset_prod (m : Multiset R[X]) : (0 : R[X]) ∉ m → m.prod.roots = m.bind roots :=
  by
  rcases m with ⟨L⟩
  simpa only [Multiset.prod_coe, quot_mk_to_coe''] using roots_list_prod L

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