no goals
l : Type ?u.919751
m : Type u_1
n : Type u_2
o : Type u_3
m' : o → Type ?u.919765
n' : o → Type ?u.919770
R : Type ?u.919773
S : Type ?u.919776
α : Type v
β : Type w
γ : Type ?u.919783
inst✝² : NonUnitalCommSemiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n α
B : Matrix m o α
x : n → α
⊢ vecMul (mulVec A x) B = vecMul x (Aᵀ ⬝ B)
rw [← vecMul_vecMul, vecMul_transpose]