natDegree_eraseLead — Mathlib

English

If f.nextCoeff ≠ 0, then eraseLead f has natDegree equal to f.natDegree − 1.

Русский

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

LaTeX

$$$\text{If } f.nextCoeff \neq 0:\quad \operatorname{natDegree}(\operatorname{eraseLead}(f)) = \operatorname{natDegree}(f) - 1$$$

Lean4

theorem natDegree_eraseLead (h : f.nextCoeff ≠ 0) : f.eraseLead.natDegree = f.natDegree - 1 :=
  by
  have := natDegree_pos_of_nextCoeff_ne_zero h
  refine f.eraseLead_natDegree_le.antisymm <| le_natDegree_of_ne_zero ?_
  rwa [eraseLead_coeff_of_ne _ (tsub_lt_self _ _).ne, ← nextCoeff_of_natDegree_pos]
  all_goals positivity

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