roots_ne_zero_of_splits — Mathlib

English

If f ∈ K[X] splits over i and natDegree f ≠ 0, then (f.map i).roots ≠ 0.

Русский

Если f ∈ K[X] распадается над i и natDegree(f) ≠ 0, то (f.map i).roots ≠ 0.

LaTeX

$$$\\forall f:\\ K[X],\\; \\text{Splits}(i,f) \\land \\operatorname{natDegree}(f) \\neq 0 \\Rightarrow (f.map i).\\text{roots} \\neq 0.$$$

Lean4

theorem roots_ne_zero_of_splits {f : K[X]} (hs : Splits i f) (hf0 : natDegree f ≠ 0) : (f.map i).roots ≠ 0 :=
  roots_ne_zero_of_splits' i hs (ne_of_eq_of_ne (natDegree_map i) hf0)

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