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
p q : R[X]
H : IsRoot q a
⊢ IsRoot (p * q) a
rw [IsRoot, eval_mul, IsRoot.def.1 H, mul_zero]