no goals
l : Type ?u.184568
m : Type u_2
n : Type ?u.184574
o : Type ?u.184577
m' : o → Type ?u.184582
n' : o → Type ?u.184587
R : Type u_1
S : Type ?u.184593
α : Type v
β : Type w
γ : Type ?u.184600
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Monoid R
inst✝³ : Mul α
inst✝² : AddCommMonoid α
inst✝¹ : DistribMulAction R α
inst✝ : IsScalarTower R α α
x : R
v w : m → α
⊢ x • v ⬝ᵥ w = x • (v ⬝ᵥ w)
simp [dotProduct, Finset.smul_sum, smul_mul_assoc]