no goals
l : Type ?u.108126
m : Type u_1
n : Type u_2
o : Type ?u.108135
m' : o → Type ?u.108140
n' : o → Type ?u.108145
R : Type ?u.108148
S : Type ?u.108151
α : Type v
β : Type w
γ : Type ?u.108158
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSemiring α
u : m → α
w : n → α
v : Matrix m n α
⊢ (fun j => u ⬝ᵥ fun i => v i j) ⬝ᵥ w = u ⬝ᵥ fun i => v i ⬝ᵥ w
simpa [dotProduct, Finset.mul_sum, Finset.sum_mul, mul_assoc] using Finset.sum_comm