∀ {V : Type u_1} {α : Type u_2} (G : SimpleGraph V) [inst : DecidableRel G.Adj] [inst_1 : Fintype V]
  [inst_2 : NonAssocSemiring α] (v : V) (vec : V → α),
  Matrix.vecMul vec (SimpleGraph.adjMatrix α G) v = ∑ u ∈ G.neighborFinset v, vec u