no goals
l : Type ?u.122679
m : Type u_1
n : Type ?u.122685
o : Type ?u.122688
m' : o → Type ?u.122693
n' : o → Type ?u.122698
R : Type ?u.122701
S : Type ?u.122704
α : Type v
β : Type w
γ : Type ?u.122711
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : AddCommMonoid α
inst✝ : CommSemigroup α
v w : m → α
⊢ v ⬝ᵥ w = w ⬝ᵥ v
simp_rw [dotProduct, mul_comm]