no goals
l : Type ?u.196339
m : Type u_2
n : Type ?u.196345
o : Type ?u.196348
m' : o → Type ?u.196353
n' : o → Type ?u.196358
R : Type u_1
S : Type ?u.196364
α : Type v
β : Type w
γ : Type ?u.196371
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Monoid R
inst✝³ : Mul α
inst✝² : AddCommMonoid α
inst✝¹ : DistribMulAction R α
inst✝ : SMulCommClass R α α
x : R
v w : m → α
⊢ v ⬝ᵥ x • w = x • (v ⬝ᵥ w)
simp [dotProduct, Finset.smul_sum, mul_smul_comm]