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