Theorem SimpleGraph.one_add_adjMatrix_add_compl_adjMatrix_eq_allOnes

Modification history

2024-04-25 07:11

Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean

chore(Combinatorics/SimpleGraph): Generalize few lemmas in `AdjMatrix` to `NonAssocSemiring α` (#12413) …

Modified SimpleGraph.one_add_adjMatrix_add_compl_adjMatrix_eq_allOnes View on Github →

2024-02-27 07:41

Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean

feat(Combinatorics/SimpleGraph/AdjMatrix): prove equation relating `adjMatrix` with its `compl` (#10992) …

Added SimpleGraph.one_add_adjMatrix_add_compl_adjMatrix_eq_allOnes View on Github →