det_lapMatrix_eq_zero — Mathlib

English

Let G be a finite graph with at least one vertex. Then the determinant of its Laplacian matrix is zero.

Русский

Пусть G — конечный граф с по крайней мере одной вершиной. Тогда определитель матрицы лапласиана G равен нулю.

LaTeX

$$$$ \\det(G.lapMatrix \\mathbb{R}) = 0 \\quad \\text{(when the vertex set is nonempty)}. $$$$

Lean4

@[simp]
theorem det_lapMatrix_eq_zero [h : Nonempty V] : (G.lapMatrix ℝ).det = 0 :=
  by
  rw [← Matrix.exists_mulVec_eq_zero_iff]
  use fun _ ↦ 1
  refine ⟨?_, (lapMatrix_mulVec_eq_zero_iff_forall_adj G).mpr fun _ _ _ ↦ rfl⟩
  rw [← Function.support_nonempty_iff]
  use Classical.choice h
  simp

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