no goals
V : Type u_2
α : Type u_1
β : Type ?u.32376
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
⊢ adjMatrix α G v ⬝ᵥ vec = ∑ u in neighborFinset G v, vec u
simp [neighborFinset_eq_filter, dotProduct, sum_filter]