mk_multiset_sum — Mathlib

English

For a multiset of elements in R, the sum under mk with denominator b equals the sum of mk of each element with b.

Русский

Для мультисетового набора элементов в R сумма под mk с знаменателем b равна сумме mk каждого элемента с тем же знаменателем.

LaTeX

$$$$ \\mathrm{mk\_multiset\_sum}(l, b) = (l.\\mathrm{map}(\\lambda a. \\mathrm{mk } a b)).\\mathrm{sum} $$$$

Lean4

theorem mk_multiset_sum (l : Multiset R) (b : M) : mk l.sum b = (l.map fun a => mk a b).sum :=
  (mkAddMonoidHom b).map_multiset_sum l

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