degree_eq_sum_if_adj — Mathlib

English

The degree matrix is the diagonal matrix with diagonal entries equal to the degrees of the corresponding vertices.

Русский

Матрица степеней является диагональной, на диагонали стоят степени соответствующих вершин.

LaTeX

$$$\degMatrix(R,G) = \operatorname{diag}(i \mapsto G.degree(i))$$$

Lean4

theorem degree_eq_sum_if_adj {R : Type*} [AddCommMonoidWithOne R] (i : V) :
    (G.degree i : R) = ∑ j : V, if G.Adj i j then 1 else 0 :=
  by
  unfold degree neighborFinset neighborSet
  rw [sum_boole, Set.toFinset_setOf]

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