roots_ne_zero_of_splits' — Mathlib

English

If f splits over i and deg(f.map i) ≠ 0, then (f.map i).roots is nonempty.

Русский

Если f распадается над i и deg(f.map i) ≠ 0, то множество корней (f.map i).roots непусто.

LaTeX

$$$\operatorname{Splits}_i(f) \wedge \deg(f.map\ i) \ne 0 \Rightarrow (f.map\ i).\text{roots} \ne \varnothing$$$

Lean4

theorem roots_ne_zero_of_splits' {f : K[X]} (hs : Splits i f) (hf0 : natDegree (f.map i) ≠ 0) : (f.map i).roots ≠ 0 :=
  let ⟨x, hx⟩ := exists_root_of_splits' i hs fun h => hf0 <| natDegree_eq_of_degree_eq_some h
  fun h => by
  rw [← eval_map] at hx
  have : f.map i ≠ 0 := by intro; simp_all
  cases h.subst ((mem_roots this).2 hx)

Похожие утверждения