smul_sum — Mathlib

English

Let N be an additive commutative monoid with an M-action distributing over addition. Then for any r ∈ M and any multiset s of N, r • (s.sum) = (s.map (r • ·)).sum.

Русский

Пусть N — коммутативный аддитивный моноид, на который распространяется действие M через сложение. Тогда для любого r∈M и мультимножества s над N верно: r • (s.sum) = (s.map (r • ·)).sum.

LaTeX

$$$\\forall {M} {N} [\\mathsf{AddCommMonoid} N] [\\mathsf{DistribSMul} M N] (r:M) (s:\\mathsf{Multiset} N),\\; r \\cdot s.sum = (s.map (r \\cdot \\cdot)).sum$$$

Lean4

theorem smul_sum {s : Multiset N} : r • s.sum = (s.map (r • ·)).sum :=
  (DistribSMul.toAddMonoidHom N r).map_multiset_sum s

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