lapMatrix_toLin'_apply_eq_zero_iff_forall_adj

English

Deprecated alias shows that Laplacian linear map equals zero iff adjacency implies equality, across all vertices, matching the prior result.

Русский

Устаревшее обозначение показывает, что линейное отображение лапласиана равно нулю тогда и только тогда, когда соседние вершины эквивалентны по значению, согласуясь с предыдущим результатом.

LaTeX

$$$G.lapMatrix Real G = 0 \iff \forall i j, G.Adj i j \Rightarrow x_i = x_j$$$

Lean4

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

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