no goals
V : Type u_2
α : Type u_1
β : Type ?u.46167
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
M : Matrix V V α
v w : V
⊢ (adjMatrix α G ⬝ M) v w = ∑ u in neighborFinset G v, M u w
simp [mul_apply, neighborFinset_eq_filter, sum_filter]