lapMatrix_toLin'_apply_eq_zero_iff_forall_reachable

Mathlib.Combinatorics.SimpleGraph.LapMatrix

URI: https://scilib.ai/kg/mathlib#SimpleGraph.lapMatrix_toLin'_apply_eq_zero_iff_forall_reachable

← MathLib Explorer

English

The Laplacian matrix is symmetric.

Русский

Лапласиан-матрица симметрична.

LaTeX

$$$ (G.lapMatrix R).IsSymm $$$

Lean4

@[deprecated lapMatrix_mulVec_eq_zero_iff_forall_reachable (since := "2025-05-18")]
theorem lapMatrix_toLin'_apply_eq_zero_iff_forall_reachable (x : V → ℝ) :
    Matrix.toLin' (G.lapMatrix ℝ) x = 0 ↔ ∀ i j : V, G.Reachable i j → x i = x j :=
  G.lapMatrix_mulVec_eq_zero_iff_forall_reachable

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru