no goals
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f✝ f : R →+* S
x : R
p : R[X]
h : IsRoot p x
⊢ IsRoot (Polynomial.map f p) (↑f x)
rw [IsRoot, eval_map, eval₂_hom, h.eq_zero, f.map_zero]