natDegree_eraseLead_add_one — Mathlib

English

If f.nextCoeff ≠ 0 then eraseLead f natDegree plus one equals f natDegree.

Русский

Если f.nextCoeff ≠ 0, то eraseLead(f).natDegree + 1 = f.natDegree.

LaTeX

$$$\operatorname{natDegree}(\operatorname{eraseLead}(f)) + 1 = \operatorname{natDegree}(f)$$$

Lean4

theorem natDegree_eraseLead_add_one (h : f.nextCoeff ≠ 0) : f.eraseLead.natDegree + 1 = f.natDegree :=
  by
  rw [natDegree_eraseLead h, tsub_add_cancel_of_le]
  exact natDegree_pos_of_nextCoeff_ne_zero h

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