English
Let u be a function m → α, w be a function n → α, and v be a matrix in M(m,n; α). Then the nested sum form satisfies the associative rearrangement:
Русский
Пусть u : m → α, w : n → α, и v ∈ M(m,n; α). Тогда сумма по j от сумм по i превращается в эквивалентную форму:
LaTeX
$$$$\sum_{j} \left(\sum_{i} u(i) \; v_{i j} \right) w(j) = \sum_{i} u(i) \left(\sum_{j} v_{i j} w(j)\right).$$$$
Lean4
theorem dotProduct_assoc [NonUnitalSemiring α] (u : m → α) (w : n → α) (v : Matrix m n α) :
(fun j => u ⬝ᵥ fun i => v i j) ⬝ᵥ w = u ⬝ᵥ fun i => v i ⬝ᵥ w := by
simpa [dotProduct, Finset.mul_sum, Finset.sum_mul, mul_assoc] using Finset.sum_comm
