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