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]
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : NoZeroSMulDivisors T S
a : S
⊢ a ∈ rootSet p S ↔ p ≠ 0 ∧ ↑(aeval a) p = 0
rw [mem_rootSet',
  (map_injective _ (NoZeroSMulDivisors.algebraMap_injective T S)).ne_iff' (Polynomial.map_zero _)]