mul_sum — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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