English
If f splits over i and deg(f.map i) ≠ 0, there exists a root x in L such that eval₂ i x f = 0.
Русский
Если f распадается над i и deg(f.map i) ≠ 0, существует корень x в L, такой что eval₂ i x f = 0.
LaTeX
$$$\operatorname{Splits}_i(f) \land \deg(f.map\ i) \ne 0 \Rightarrow \exists x\in L,\ \operatorname{eval}_i(x,f) = 0$$$
Lean4
theorem exists_root_of_splits' {f : K[X]} (hs : Splits i f) (hf0 : degree (f.map i) ≠ 0) : ∃ x, eval₂ i x f = 0 :=
letI := Classical.decEq L
if hf0' : f.map i = 0 then by simp [eval₂_eq_eval_map, hf0']
else
let ⟨g, hg⟩ :=
WfDvdMonoid.exists_irreducible_factor (show ¬IsUnit (f.map i) from mt isUnit_iff_degree_eq_zero.1 hf0) hf0'
let ⟨x, hx⟩ := exists_root_of_degree_eq_one (hs.resolve_left hf0' hg.1 hg.2)
let ⟨i, hi⟩ := hg.2
⟨x, by rw [← eval_map, hi, eval_mul, show _ = _ from hx, zero_mul]⟩
