English
For a finite index set, the root property of a product of polynomials is equivalent to the existence of an index i with a root of p_i at x (in appropriate domain assumptions).
Русский
Для конечного множества индексов соблюдается эквивалентность: корень произведения полиномов существует тогда и только тогда, когда существует индекс i, для которого p_i имеет корень в x (при соответствующих предположениях).
LaTeX
$$$\\IsRoot(\\prod_{j\\in s} p_j, x) \\iff \\exists i\\in s, \\IsRoot(p_i, x)$$$
Lean4
theorem isRoot_prod {R} [CommSemiring R] [IsDomain R] {ι : Type*} (s : Finset ι) (p : ι → R[X]) (x : R) :
IsRoot (∏ j ∈ s, p j) x ↔ ∃ i ∈ s, IsRoot (p i) x := by simp only [IsRoot, eval_prod, Finset.prod_eq_zero_iff]
