apply_diag_ne — Mathlib

English

For an adjacency matrix of a simple graph, the diagonal entries are not equal to 1.

Русский

Для диагональных элементов матрицы смежности простого графа диагональные элементы не равны 1.

LaTeX

$$$A.IsAdjMatrix \Rightarrow \forall i: V, A_{ii} \neq 1$$$

Lean4

@[simp]
theorem apply_diag_ne [MulZeroOneClass α] [Nontrivial α] (h : IsAdjMatrix A) (i : V) : ¬A i i = 1 := by
  simp [h.apply_diag i]

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