Theorem SimpleGraph.one_add_adjMatrix_add_compl_adjMatrix_eq_allOnes

Modification history

2026-03-04 18:26
Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean
feat(Combinatorics/SimpleGraph/AdjMatrix): adjacency matrix API (#34601)
Deleted SimpleGraph.one_add_adjMatrix_add_compl_adjMatrix_eq_allOnesView on Github →
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_allOnesView 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_allOnesView on Github →