no goals
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f : K[X]
hs : Splits i f
hf0 : degree (map i f) ≠ 0
hf0' : map i f = 0
⊢ ∃ x, eval₂ i x f = 0
simp [eval₂_eq_eval_map, hf0']
no goals
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
f : K[X]
hs : Splits i✝ f
hf0 : degree (map i✝ f) ≠ 0
hf0' : ¬map i✝ f = 0
g : L[X]
hg : Irreducible g ∧ g ∣ map i✝ f
x : L
hx : IsRoot g x
i : L[X]
hi : map i✝ f = g * i
⊢ eval₂ i✝ x f = 0
rw [← eval_map, hi, eval_mul, show _ = _ from hx, MulZeroClass.zero_mul]