l : Type ?u.840566
m : Type u_2
n : Type u_1
o : Type ?u.840575
m' : o → Type ?u.840580
n' : o → Type ?u.840585
R : Type u_3
S : Type ?u.840591
α : Type v
β : Type w
γ : Type ?u.840598
inst✝³ : NonUnitalNonAssocSemiring α
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : NonUnitalSemiring R
v : m → R
A : Matrix m n R
w : n → R
⊢ ∑ x : m, ∑ x_1 : n, v x * (A x x_1 * w x_1) = ∑ x : n, ∑ x_1 : m, v x_1 * (A x_1 x * w x)
l : Type ?u.840566
m : Type u_2
n : Type u_1
o : Type ?u.840575
m' : o → Type ?u.840580
n' : o → Type ?u.840585
R : Type u_3
S : Type ?u.840591
α : Type v
β : Type w
γ : Type ?u.840598
inst✝³ : NonUnitalNonAssocSemiring α
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : NonUnitalSemiring R
v : m → R
A : Matrix m n R
w : n → R
⊢ v ⬝ᵥ mulVec A w = vecMul v A ⬝ᵥ w
simp only [dotProduct, vecMul, mulVec, Finset.mul_sum, Finset.sum_mul, mul_assoc]
no goals
l : Type ?u.840566
m : Type u_2
n : Type u_1
o : Type ?u.840575
m' : o → Type ?u.840580
n' : o → Type ?u.840585
R : Type u_3
S : Type ?u.840591
α : Type v
β : Type w
γ : Type ?u.840598
inst✝³ : NonUnitalNonAssocSemiring α
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : NonUnitalSemiring R
v : m → R
A : Matrix m n R
w : n → R
⊢ ∑ x : m, ∑ x_1 : n, v x * (A x x_1 * w x_1) = ∑ x : n, ∑ x_1 : m, v x_1 * (A x_1 x * w x)
exact Finset.sum_comm