incMatrix_mul_transpose_diag — Mathlib

English

The product of the incidence matrix with its transpose has, on the diagonal, entries equal to the degrees of the corresponding vertices.

Русский

Произведение матрицы инцидентности и её транспонированной имеет на диагонали значения степеней вершин.

LaTeX

$$$\forall {R} {\alpha} (G : SimpleGraph \alpha) [Fintype (Sym2 \alpha)] {a : \alpha},\; (G.incMatrix R * (G.incMatrix R)^T) a a = G.degree a$$$

Lean4

theorem incMatrix_mul_transpose_diag [Fintype (Sym2 α)] [Fintype (neighborSet G a)] :
    (G.incMatrix R * (G.incMatrix R)ᵀ) a a = G.degree a :=
  by
  rw [← sum_incMatrix_apply]
  simp only [mul_apply, incMatrix_apply', transpose_apply, mul_ite, mul_one, mul_zero]
  simp_all only [ite_true, sum_boole]

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