no goals
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
⊢ Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots p)) =
    Finset.prod (Multiset.toFinset (roots p)) fun a => (X - ↑C a) ^ rootMultiplicity a p
simp only [count_roots, Finset.prod_multiset_map_count]