no goals
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q✝ p q : R[X]
hpq : p * q ≠ 0
r : R
⊢ count r (roots (p * q)) = count r (roots p + roots q)
rw [count_add, count_roots, count_roots, count_roots, rootMultiplicity_mul hpq]