support_sum — Mathlib

English

Sum of a finite family: the sum equals the Finset sum of coefficients times monomials.

Русский

Сумма по конечному набору равна сумме по индексам коэффициентов и мономов.

LaTeX

$$$ p.sum b = \\\\sum m \\\\in p.support, \\\\ b m (p.coeff m) $$$

Lean4

theorem support_sum {α : Type*} [DecidableEq σ] {s : Finset α} {f : α → MvPolynomial σ R} :
    (∑ x ∈ s, f x).support ⊆ s.biUnion fun x => (f x).support :=
  Finsupp.support_finset_sum

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