smul_sum — Mathlib

English

Let r act on a list of elements of an additive monoid N. Then scalar multiplication distributes over the sum of the list: r • (l.sum) = (map (r • ·) l).sum.

Русский

Пусть r действует на список элементов аддитивного моноида N. Тогда скалярное умножение распределяется по сумме списка: r • (l.sum) = (map (r • ·) l).sum.

LaTeX

$$$\\forall {M} {N} [\\mathsf{AddMonoid}\\ N] [\\mathsf{DistribSMul}\\ M\\ N] (r:M) (l:\\text{List }N),\\; r \\cdot l.sum = (l.map (r \\cdot \\cdot)).sum$$$

Lean4

theorem smul_sum {r : M} {l : List N} : r • l.sum = (l.map (r • ·)).sum :=
  map_list_sum (DistribSMul.toAddMonoidHom N r) l

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