feat(combinatorics/adjacency_matrix): defines adjacency matrices of simple graphs (#3672)
feat(combinatorics/adjacency_matrix): defines adjacency matrices of simple graphs (#3672)

defines the adjacency matrix of a simple graph
proves lemmas about adjacency matrix that will form the bulk of the proof of the friendship theorem (freek 83)



Co-authored-by: Aaron Anderson <a21c0a60b4199b3dbd50b4746a00587bbbcedcf1@gmail.com>

leanprover-community/mathlib,leanprover-community/mathlib