no goals
R✝ : Type u
S : Type v
T : Type w
ι✝ : Type y
a b : R✝
m n : ℕ
inst✝³ : CommSemiring R✝
p✝ q : R✝[X]
x✝ : R✝
inst✝² : CommSemiring S
f : R✝ →+* S
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ι : Type u_2
s : Finset ι
p : ι → R[X]
x : R
⊢ IsRoot (∏ j in s, p j) x ↔ ∃ i, i ∈ s ∧ IsRoot (p i) x
simp only [IsRoot, eval_prod, Finset.prod_eq_zero_iff]