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
a : S
⊢ a ∈ rootSet p S ↔ map (algebraMap T S) p ≠ 0 ∧ ↑(aeval a) p = 0
rw [rootSet, Finset.mem_coe, mem_toFinset, mem_roots', IsRoot.def, ← eval₂_eq_eval_map,
  aeval_def]