single_multiset_sum — Mathlib

English

In a multiset s of M, the coefficient-at-a of single a applied to s.sum equals the sum (over s) of single a applied to each element.

Русский

В мультисете s над M координата a удовлетворяет: single a (s.sum) = s.map (single a).sum.

LaTeX

$$$$ \\mathrm{single}(a, s.\\sum) = s.\\sum (\\mathrm{single}(a)) $$$$

Lean4

theorem single_multiset_sum [AddCommMonoid M] (s : Multiset M) (a : α) : single a s.sum = (s.map (single a)).sum :=
  Multiset.induction_on s (single_zero _) fun a s ih => by
    rw [Multiset.sum_cons, single_add, ih, Multiset.map_cons, Multiset.sum_cons]

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