no goals
k : Type u
inst✝² : Field k
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsAlgClosed k
f : R →+* k
hf : Function.Injective ↑f
p : R[X]
hp : degree p ≠ 0
⊢ degree (map f p) ≠ 0
rwa [degree_map_eq_of_injective hf]
no goals
k : Type u
inst✝² : Field k
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsAlgClosed k
f : R →+* k
hf : Function.Injective ↑f
p : R[X]
hp : degree p ≠ 0
x : k
hx : IsRoot (map f p) x
⊢ eval₂ f x p = 0
rwa [eval₂_eq_eval_map, ← IsRoot]