degMatrix — Mathlib

English

The Laplacian of a graph is the difference between its degree matrix and its adjacency matrix: L = D - A.

Русский

Лапласиан графа равен разности диагональной матрицы степеней и матрицы смежности: L = D - A.

LaTeX

$$$\mathrm{lapMatrix}(R,G) = G.degMatrix R \; - \; G.adjMatrix R$$$

Lean4

/-- The diagonal matrix consisting of the degrees of the vertices in the graph. -/
def degMatrix [AddMonoidWithOne R] : Matrix V V R :=
  Matrix.diagonal (G.degree ·)

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