no goals
l : Type ?u.917788
m : Type u_3
n : Type u_1
o : Type u_2
m' : o → Type ?u.917802
n' : o → Type ?u.917807
R : Type ?u.917810
S : Type ?u.917813
α : Type v
β : Type w
γ : Type ?u.917820
inst✝² : NonUnitalCommSemiring α
inst✝¹ : Fintype n
inst✝ : Fintype o
A : Matrix m n α
B : Matrix o n α
x : o → α
⊢ mulVec A (vecMul x B) = mulVec (A ⬝ Bᵀ) x
rw [← mulVec_mulVec, mulVec_transpose]