eraseLead_natDegree_lt — Mathlib

English

If #Supp(f) ≥ 2, then (eraseLead f).natDegree < f.natDegree.

Русский

Если число элементов опоры f не менее 2, то natDegree(eraseLead(f)) < natDegree(f).

LaTeX

$$$2 \le |\operatorname{Supp}(f)| \Rightarrow (\operatorname{eraseLead}(f)).\operatorname{natDegree} < f.\operatorname{natDegree}$$$

Lean4

theorem eraseLead_natDegree_lt (f0 : 2 ≤ #f.support) : (eraseLead f).natDegree < f.natDegree :=
  lt_of_le_of_ne eraseLead_natDegree_le_aux <|
    ne_natDegree_of_mem_eraseLead_support <| natDegree_mem_support_of_nonzero <| eraseLead_ne_zero f0

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