natDegree_divX_eq_natDegree_tsub_one

English

For any polynomial p, the natural degree of p.divX is natDegree(p) minus 1.

Русский

Для любого полинома p натуральная степень p.divX равна natDegree(p) минус 1.

LaTeX

$$$\\operatorname{natDegree}(p.divX) = \\operatorname{natDegree}(p) - 1$$$

Lean4

theorem natDegree_divX_eq_natDegree_tsub_one : p.divX.natDegree = p.natDegree - 1 :=
  by
  apply map_natDegree_eq_sub (φ := divX_hom)
  · intro f
    simpa [divX_hom, divX_eq_zero_iff] using eq_C_of_natDegree_eq_zero
  · intro n c c0
    rw [← C_mul_X_pow_eq_monomial, divX_hom_toFun, divX_C_mul, divX_X_pow]
    split_ifs with n0
    · simp [n0]
    · exact natDegree_C_mul_X_pow (n - 1) c c0

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