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