eraseLead_add_monomial_natDegree_leadingCoeff

English

Subtracting the leading monomial from a polynomial and then adding back the leading monomial recovers the original polynomial.

Русский

Избавление от ведущего монома и последующее добавление ведущего монома восстанавливает исходный многочлен.

LaTeX

$$f.eraseLead + monomial(f.natDegree) f.leadingCoeff = f$$

Lean4

@[simp]
theorem eraseLead_add_monomial_natDegree_leadingCoeff (f : R[X]) :
    f.eraseLead + monomial f.natDegree f.leadingCoeff = f :=
  (add_comm _ _).trans (f.monomial_add_erase _)

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