one_add_adjMatrix_add_compl_adjMatrix_eq_allOnes

English

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

Русский

Сумма единичной матрицы, матрицы смежности и её комплемента равна матрице all-ones.

LaTeX

$$1 + G.adjMatrix α + (G.adjMatrix α).compl = Matrix.of (fun _ _ => 1)$$

Lean4

/-- The sum of the identity, the adjacency matrix, and its complement is the all-ones matrix. -/
theorem one_add_adjMatrix_add_compl_adjMatrix_eq_allOnes [DecidableEq V] [DecidableEq α] [AddMonoidWithOne α] :
    1 + G.adjMatrix α + (G.adjMatrix α).compl = Matrix.of fun _ _ ↦ 1 :=
  by
  ext i j
  unfold Matrix.compl
  rw [of_apply, add_apply, adjMatrix_apply, add_apply, adjMatrix_apply, one_apply]
  by_cases h : G.Adj i j
  · aesop
  · split_ifs <;> simp_all

Похожие утверждения