l : Type ?u.894994
m : Type ?u.894997
n : Type u_1
o : Type ?u.895003
m' : o → Type ?u.895008
n' : o → Type ?u.895013
R : Type ?u.895016
S : Type ?u.895019
α : Type v
β : Type w
γ : Type ?u.895026
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype n
A B C : Matrix n n α
i j : n
⊢ (A ⬝ (B ⬝ C)) i j = A i ⬝ᵥ mulVec B (Cᵀ j)
l : Type ?u.894994
m : Type ?u.894997
n : Type u_1
o : Type ?u.895003
m' : o → Type ?u.895008
n' : o → Type ?u.895013
R : Type ?u.895016
S : Type ?u.895019
α : Type v
β : Type w
γ : Type ?u.895026
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype n
A B C : Matrix n n α
i j : n
⊢ (A ⬝ B ⬝ C) i j = A i ⬝ᵥ mulVec B (Cᵀ j)
rw [Matrix.mul_assoc]
l : Type ?u.894994
m : Type ?u.894997
n : Type u_1
o : Type ?u.895003
m' : o → Type ?u.895008
n' : o → Type ?u.895013
R : Type ?u.895016
S : Type ?u.895019
α : Type v
β : Type w
γ : Type ?u.895026
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype n
A B C : Matrix n n α
i j : n
⊢ ∑ x : n, A i x * ∑ j_1 : n, B x j_1 * C j_1 j = ∑ x : n, A i x * ∑ x_1 : n, B x x_1 * Cᵀ j x_1
l : Type ?u.894994
m : Type ?u.894997
n : Type u_1
o : Type ?u.895003
m' : o → Type ?u.895008
n' : o → Type ?u.895013
R : Type ?u.895016
S : Type ?u.895019
α : Type v
β : Type w
γ : Type ?u.895026
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype n
A B C : Matrix n n α
i j : n
⊢ (A ⬝ (B ⬝ C)) i j = A i ⬝ᵥ mulVec B (Cᵀ j)
simp only [mul_apply, dotProduct, mulVec]
no goals
l : Type ?u.894994
m : Type ?u.894997
n : Type u_1
o : Type ?u.895003
m' : o → Type ?u.895008
n' : o → Type ?u.895013
R : Type ?u.895016
S : Type ?u.895019
α : Type v
β : Type w
γ : Type ?u.895026
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype n
A B C : Matrix n n α
i j : n
⊢ ∑ x : n, A i x * ∑ j_1 : n, B x j_1 * C j_1 j = ∑ x : n, A i x * ∑ x_1 : n, B x x_1 * Cᵀ j x_1
rfl