sum_mul — Mathlib

English

Sum distributes over right multiplication on the left: (∑_{a∈s} f(a)) · M = ∑_{a∈s} (f(a) · M).

Русский

Сумма распадается по умножению слева: (∑_{a∈s} f(a)) · M = ∑_{a∈s} (f(a) · M).

LaTeX

$$$\\left(\\sum_{a \\in s} f(a)\\right) \\cdot M = \\sum_{a \\in s} f(a) \\cdot M$$$

Lean4

protected theorem sum_mul [Fintype m] (s : Finset β) (f : β → Matrix l m α) (M : Matrix m n α) :
    (∑ a ∈ s, f a) * M = ∑ a ∈ s, f a * M :=
  map_sum (addMonoidHomMulRight M) f s

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