Commit 2026-03-04 18:26 bf4bf08e

View on Github →

feat(Combinatorics/SimpleGraph/AdjMatrix): adjacency matrix API (#34601)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean

added theorem Matrix.IsAdjMatrix.compl_compl

added theorem Matrix.IsAdjMatrix.compl_inj

added theorem Matrix.IsAdjMatrix.hadamard_self

added theorem Matrix.compl_of_one_sub_one

added theorem Matrix.compl_zero

added theorem Matrix.compl_zero_eq_of_one_sub_one

added theorem SimpleGraph.IsCompl.adjMatrix_add_adjMatrix_eq_adjMatrix_completeGraph

added theorem SimpleGraph.adjMatrix_add_compl_adjMatrix_eq_adjMatrix_completeGraph

added theorem SimpleGraph.adjMatrix_completeGraph_eq_of_one_sub_one

added theorem SimpleGraph.adjMatrix_hadamard_diagonal

added theorem SimpleGraph.adjMatrix_hadamard_intCast

added theorem SimpleGraph.adjMatrix_hadamard_natCast

added theorem SimpleGraph.adjMatrix_hadamard_ofNat

added theorem SimpleGraph.adjMatrix_hadamard_one

added theorem SimpleGraph.adjMatrix_hadamard_self

added theorem SimpleGraph.compl_adjMatrix_completeGraph

added theorem SimpleGraph.compl_adjMatrix_eq_adjMatrix_compl

added theorem SimpleGraph.diag_adjMatrix

added theorem SimpleGraph.diagonal_hadamard_adjMatrix

added theorem SimpleGraph.intCast_hadamard_adjMatrix

modified theorem SimpleGraph.isAdjMatrix_adjMatrix

added theorem SimpleGraph.natCast_card_dart_eq_dotProduct

added theorem SimpleGraph.natCast_hadamard_adjMatrix

added theorem SimpleGraph.ofNat_hadamard_adjMatrix

deleted theorem SimpleGraph.one_add_adjMatrix_add_compl_adjMatrix_eq_allOnes

added theorem SimpleGraph.one_add_adjMatrix_add_compl_adjMatrix_eq_of_one

added theorem SimpleGraph.one_hadamard_adjMatrix