l m n : ℕ
α : Type u_1
β : Type ?u.51370
inst✝ : NonUnitalNonAssocSemiring α
v : Fin l → α
A : Matrix (Fin l) (Fin m) α
⊢ (fun x => v ⬝ᵥ Aᵀ x) = vecMul v A
l m n : ℕ
α : Type u_1
β : Type ?u.51370
inst✝ : NonUnitalNonAssocSemiring α
v : Fin l → α
A : Matrix (Fin l) (Fin m) α
⊢ vecMulᵣ v A = vecMul v A
simp [vecMulᵣ, Function.comp]
no goals
l m n : ℕ
α : Type u_1
β : Type ?u.51370
inst✝ : NonUnitalNonAssocSemiring α
v : Fin l → α
A : Matrix (Fin l) (Fin m) α
⊢ (fun x => v ⬝ᵥ Aᵀ x) = vecMul v A
rfl