no goals
R : Type u
S : Type v
k : Type y
A : Type z
a✝ b : R
n✝ : ℕ
inst✝³ : Field R
p q : R[X]
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
n : ℕ
hn : n ≠ 0
a : R
ha : a ≠ 0
⊢ rootSet (↑(monomial n) a) S = {0}
rw [rootSet, map_monomial, roots_monomial ((_root_.map_ne_zero (algebraMap R S)).2 ha),
  Multiset.toFinset_nsmul _ _ hn, Multiset.toFinset_singleton, Finset.coe_singleton]