case h
l : Type ?u.884429
m : Type u_2
n : Type u_1
o : Type u_3
m' : o → Type ?u.884443
n' : o → Type ?u.884448
R : Type ?u.884451
S : Type ?u.884454
α : Type v
β : Type w
γ : Type ?u.884461
inst✝² : NonUnitalSemiring α
inst✝¹ : Fintype n
inst✝ : Fintype m
v : m → α
M : Matrix m n α
N : Matrix n o α
x✝ : o
⊢ vecMul (vecMul v M) N x✝ = vecMul v (M ⬝ N) x✝
l : Type ?u.884429
m : Type u_2
n : Type u_1
o : Type u_3
m' : o → Type ?u.884443
n' : o → Type ?u.884448
R : Type ?u.884451
S : Type ?u.884454
α : Type v
β : Type w
γ : Type ?u.884461
inst✝² : NonUnitalSemiring α
inst✝¹ : Fintype n
inst✝ : Fintype m
v : m → α
M : Matrix m n α
N : Matrix n o α
⊢ vecMul (vecMul v M) N = vecMul v (M ⬝ N)
ext
no goals
case h
l : Type ?u.884429
m : Type u_2
n : Type u_1
o : Type u_3
m' : o → Type ?u.884443
n' : o → Type ?u.884448
R : Type ?u.884451
S : Type ?u.884454
α : Type v
β : Type w
γ : Type ?u.884461
inst✝² : NonUnitalSemiring α
inst✝¹ : Fintype n
inst✝ : Fintype m
v : m → α
M : Matrix m n α
N : Matrix n o α
x✝ : o
⊢ vecMul (vecMul v M) N x✝ = vecMul v (M ⬝ N) x✝
apply dotProduct_assoc