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
p : T[X]
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a : S
h : a ∈ rootSet p S
hf : p = 0
⊢ False
rwa [hf, rootSet_zero] at h