no goals
l : Type ?u.1326869
m : Type u_4
n : Type u_3
o : Type ?u.1326878
m' : o → Type ?u.1326883
n' : o → Type ?u.1326888
R : Type u_1
S : Type u_2
α : Type v
β : Type w
γ : Type ?u.1326901
inst✝⁴ : Fintype n
inst✝³ : NonAssocSemiring α
inst✝² : NonAssocSemiring β
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
f : R →+* S
M : Matrix n m R
v : n → R
i : m
⊢ ↑f (vecMul v M i) = vecMul (↑f ∘ v) (map M ↑f) i
simp only [Matrix.vecMul, Matrix.map_apply, RingHom.map_dotProduct, Function.comp]