sum_def — Mathlib

English

The sum over a Finset of polynomials equals the Finset sum of their sums by coefficient.

Русский

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

LaTeX

$$$ p.sum b = p.support.sum (fun m => b m (coeff m p)) $$$

Lean4

theorem sum_def {A} [AddCommMonoid A] {p : MvPolynomial σ R} {b : (σ →₀ ℕ) → R → A} :
    p.sum b = ∑ m ∈ p.support, b m (p.coeff m) := by simp [support, Finsupp.sum, coeff]

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