no goals
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
hp : p ≠ 0
⊢ Set.Finite {x | IsRoot p x}
simpa only [← Finset.setOf_mem, Multiset.mem_toFinset, mem_roots hp]
  using p.roots.toFinset.finite_toSet