support_sum_monomial_coeff — Mathlib

English

Summing monomials over the support with their coefficients recovers the original polynomial.

Русский

Суммирование мономиалов по опоре с коэффициентами восстанавливает исходный полином.

LaTeX

$$$ \\sum_{v \\in p.\\mathrm{support}} \\mathrm{monomial}(v, p.\\mathrm{coeff} v) = p. $$$

Lean4

@[simp]
theorem support_sum_monomial_coeff (p : MvPolynomial σ R) : (∑ v ∈ p.support, monomial v (coeff v p)) = p :=
  Finsupp.sum_single p

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