Theorems · Theorem · combinatorics

SimpleGraph.one_add_adjMatrix_add_compl_adjMatrix_eq_of_one

∀ (α : Type u_1) {V : Type u_2} (G : SimpleGraph V) [inst : DecidableRel G.Adj] [inst_1 : DecidableEq V]
  [inst_2 : DecidableEq α] [inst_3 : AddMonoid α] [inst_4 : One α],
  1 + SimpleGraph.adjMatrix α G + (SimpleGraph.adjMatrix α G).compl = Matrix.of 1

The sum of the identity, the adjacency matrix, and its complement is the all-ones matrix.

Defined in

Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Cited by

1 results in Mathlib

Foundations

Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableRelDecidableEqDecidableEqAddMonoidOne