Commit 2023-04-05 14:36 52872ce4

View on Github →

feat: port Combinatorics.SimpleGraph.AdjMatrix (#3287)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean

added theorem Matrix.IsAdjMatrix.adjMatrix_toGraph_eq

added theorem Matrix.IsAdjMatrix.apply_diag_ne

added theorem Matrix.IsAdjMatrix.apply_ne_one_iff

added theorem Matrix.IsAdjMatrix.apply_ne_zero_iff

added theorem Matrix.IsAdjMatrix.compl

added def Matrix.IsAdjMatrix.toGraph

added theorem Matrix.IsAdjMatrix.toGraph_compl_eq

added structure Matrix.IsAdjMatrix

added def Matrix.compl

added theorem Matrix.compl_apply

added theorem Matrix.compl_apply_diag

added theorem Matrix.isAdjMatrix_compl

added theorem Matrix.isSymm_compl

added def SimpleGraph.adjMatrix

added theorem SimpleGraph.adjMatrix_apply

added theorem SimpleGraph.adjMatrix_dotProduct

added theorem SimpleGraph.adjMatrix_mulVec_apply

added theorem SimpleGraph.adjMatrix_mulVec_const_apply

added theorem SimpleGraph.adjMatrix_mulVec_const_apply_of_regular

added theorem SimpleGraph.adjMatrix_mul_apply

added theorem SimpleGraph.adjMatrix_mul_self_apply_self

added theorem SimpleGraph.adjMatrix_pow_apply_eq_card_walk

added theorem SimpleGraph.adjMatrix_vecMul_apply

added theorem SimpleGraph.dotProduct_adjMatrix

added theorem SimpleGraph.isAdjMatrix_adjMatrix

added theorem SimpleGraph.isSymm_adjMatrix

added theorem SimpleGraph.mul_adjMatrix_apply

added theorem SimpleGraph.toGraph_adjMatrix_eq

added theorem SimpleGraph.trace_adjMatrix

added theorem SimpleGraph.transpose_adjMatrix