coeff_sum — Mathlib

English

The coefficient of a finite sum equals the finite sum of coefficients: coeff m (∑ x∈s f x) = ∑ x∈s coeff m (f x).

Русский

Коэффициент при m суммы по элементам множества s равен сумме коэффициентов по каждому элементу: coeff m (∑ f x) = ∑ coeff m (f x).

LaTeX

$$$\mathrm{coeff}\;m (\sum_{x\in s} f\ x) = \sum_{x\in s} \mathrm{coeff}\;m (f\ x)$$$

Lean4

theorem coeff_sum {X : Type*} (s : Finset X) (f : X → MvPolynomial σ R) (m : σ →₀ ℕ) :
    coeff m (∑ x ∈ s, f x) = ∑ x ∈ s, coeff m (f x) :=
  map_sum (@coeffAddMonoidHom R σ _ _) _ s

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