no goals
V : Type u_2
α : Type u_1
β : Type ?u.58967
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
i : V
⊢ (adjMatrix α G ⬝ adjMatrix α G) i i = ↑(degree G i)
simp [degree]