no goals
l : Type ?u.1289823
m : Type ?u.1289826
n : Type u_3
o : Type ?u.1289832
m' : o → Type ?u.1289837
n' : o → Type ?u.1289842
R : Type u_1
S : Type u_2
α : Type v
β : Type w
γ : Type ?u.1289855
inst✝⁴ : Fintype n
inst✝³ : NonAssocSemiring α
inst✝² : NonAssocSemiring β
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
f : R →+* S
v w : n → R
⊢ ↑f (v ⬝ᵥ w) = ↑f ∘ v ⬝ᵥ ↑f ∘ w
simp only [Matrix.dotProduct, f.map_sum, f.map_mul, Function.comp]