Commit 2026-05-31 20:29 bff3d51d

View on Github →

feat(Combinatorics/SimpleGraph/AdjMatrix): submatrices and homomorphisms (#36388)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean

added theorem Matrix.IsAdjMatrix.diag_eq_zero

added theorem Matrix.IsAdjMatrix.reindex

added def Matrix.IsAdjMatrix.toGraphReindexIso

added def Matrix.IsAdjMatrix.toGraphSubmatrixEmbedding

added theorem Matrix.IsAdjMatrix.toGraphSubmatrixEmbedding_apply

added def Matrix.IsAdjMatrix.toGraphSubmatrixHom

added theorem Matrix.isAdjMatrix_reindex_iff

added theorem Matrix.isAdjMatrix_submatrix_iff

added theorem SimpleGraph.Embedding.submatrix_adjMatrix

added theorem SimpleGraph.Iso.reindex_adjMatrix

modified theorem SimpleGraph.diag_adjMatrix