case h
l : Type ?u.867277
m : Type u_4
n : Type u_1
o : Type ?u.867286
m' : o → Type ?u.867291
n' : o → Type ?u.867296
R : Type u_2
S : Type u_3
α : Type v
β : Type w
γ : Type ?u.867309
inst✝⁵ : NonUnitalNonAssocSemiring α
inst✝⁴ : Fintype n
inst✝³ : Monoid R
inst✝² : NonUnitalNonAssocSemiring S
inst✝¹ : DistribMulAction R S
inst✝ : SMulCommClass R S S
M : Matrix m n S
b : R
v : n → S
i : m
⊢ mulVec M (b • v) i = (b • mulVec M v) i
l : Type ?u.867277
m : Type u_4
n : Type u_1
o : Type ?u.867286
m' : o → Type ?u.867291
n' : o → Type ?u.867296
R : Type u_2
S : Type u_3
α : Type v
β : Type w
γ : Type ?u.867309
inst✝⁵ : NonUnitalNonAssocSemiring α
inst✝⁴ : Fintype n
inst✝³ : Monoid R
inst✝² : NonUnitalNonAssocSemiring S
inst✝¹ : DistribMulAction R S
inst✝ : SMulCommClass R S S
M : Matrix m n S
b : R
v : n → S
⊢ mulVec M (b • v) = b • mulVec M v
ext i
no goals
case h
l : Type ?u.867277
m : Type u_4
n : Type u_1
o : Type ?u.867286
m' : o → Type ?u.867291
n' : o → Type ?u.867296
R : Type u_2
S : Type u_3
α : Type v
β : Type w
γ : Type ?u.867309
inst✝⁵ : NonUnitalNonAssocSemiring α
inst✝⁴ : Fintype n
inst✝³ : Monoid R
inst✝² : NonUnitalNonAssocSemiring S
inst✝¹ : DistribMulAction R S
inst✝ : SMulCommClass R S S
M : Matrix m n S
b : R
v : n → S
i : m
⊢ mulVec M (b • v) i = (b • mulVec M v) i
simp only [mulVec, dotProduct, Finset.smul_sum, Pi.smul_apply, mul_smul_comm]