as_sum — Mathlib

English

Any polynomial p equals the sum over its support of monomials with the corresponding coefficients.

Русский

Любой полином p равен сумме по опоре мономиалов с соответствующими коэффициентами.

LaTeX

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

Lean4

theorem as_sum (p : MvPolynomial σ R) : p = ∑ v ∈ p.support, monomial v (coeff v p) :=
  (support_sum_monomial_coeff p).symm

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