English
Let f : ι → R[X] be a family of polynomials and s a finite set. If the product ∏_{i∈s} f(i) is nonzero, then the roots of the product are precisely the union of the roots of the factors: rootSet of the product equals the union of the root sets of each f(i).
Русский
Пусть f: ι → R[X] и на множестве s дано произведение. Если произведение не равно нулю, корни произведения совпадают с объединением корней каждого множителя: rootSet произведения равен объединению корней каждого f(i).
LaTeX
$$$ \operatorname{rootSet} (\prod_{i \in s} f(i)) S = \bigcup_{i \in s} (f(i)).rootSet S, \quad (s \prod f) \neq 0 $$$
Lean4
theorem rootSet_prod [CommRing S] [IsDomain S] [Algebra R S] {ι : Type*} (f : ι → R[X]) (s : Finset ι)
(h : s.prod f ≠ 0) : (s.prod f).rootSet S = ⋃ i ∈ s, (f i).rootSet S := by
classical
simp only [rootSet, aroots, ← Finset.mem_coe]
rw [Polynomial.map_prod, roots_prod, Finset.bind_toFinset, s.val_toFinset, Finset.coe_biUnion]
rwa [← Polynomial.map_prod, Ne, Polynomial.map_eq_zero]
