monomial_add_erase — Mathlib

English

For any polynomial p and index n, the sum of the nth coefficient monomial and the remainder p.erase n equals p: monomial n (coeff p n) + p.erase n = p.

Русский

Для любого многочлена p и индекса n сумма монома с коэффициентом при n и остаток p.erase n равны p: monomial n (coeff p n) + p.erase n = p.

LaTeX

$$$\\text{monomial}_n(\\text{coeff } p\\ n) + p.erase n = p$$$

Lean4

theorem monomial_add_erase (p : R[X]) (n : ℕ) : monomial n (coeff p n) + p.erase n = p :=
  toFinsupp_injective <| by
    rw [toFinsupp_add, toFinsupp_monomial, toFinsupp_erase, coeff]
    exact Finsupp.single_add_erase _ _

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