mk_list_sum — Mathlib

English

Summing images of a list under mk with a common denominator equals the image of the sum.

Русский

Сумма образов списка под mk с общим знаменателем равна образу суммы.

LaTeX

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

Lean4

theorem mk_list_sum (l : List R) (b : M) : mk l.sum b = (l.map fun a => mk a b).sum :=
  map_list_sum (mkAddMonoidHom b) l

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