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]
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a : T
⊢ rootSet (↑C a) S = ∅
rw [rootSet_def, map_C, roots_C, Multiset.toFinset_zero, Finset.coe_empty]