no goals
V : Type u_2
α : Type u_1
β : Type ?u.42278
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
⊢ mulVec (adjMatrix α G) vec v = ∑ u in neighborFinset G v, vec u
rw [mulVec, adjMatrix_dotProduct]