multiset_sum_sum_index — Mathlib

English

Sum over a multiset of finsupps commutes with summing the sums of each finsupp.

Русский

Сумма по мультимножеству финспп коммутирует со сложением сумм каждого элемента.

LaTeX

$$$$ f.sum.sum h = (f.map (\lambda g : α →₀ M => g.sum h)).sum. $$$$

Lean4

theorem multiset_sum_sum_index [AddCommMonoid M] [AddCommMonoid N] (f : Multiset (α →₀ M)) (h : α → M → N)
    (h₀ : ∀ a, h a 0 = 0) (h₁ : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂) :
    f.sum.sum h = (f.map fun g : α →₀ M => g.sum h).sum :=
  Multiset.induction_on f rfl fun a s ih => by
    rw [Multiset.sum_cons, Multiset.map_cons, Multiset.sum_cons, sum_add_index' h₀ h₁, ih]

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