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 k
inst✝ : IsDomain k
f : R →+* k
x : k
hp : p ≠ 0
⊢ x ∈ roots (map f p) ↔ eval₂ f x p = 0
rw [mem_roots (map_ne_zero hp), IsRoot, Polynomial.eval_map]