card_connectedComponent_eq_finrank_ker_toLin'_lapMatrix

English

The number of connected components of G equals the finrank over ℝ of the kernel of Matrix.toLin'(G.lapMatrix).

Русский

Число связных компонент графа G равно размерности ядра над ℝ линейного отображения Matrix.toLin'(G.lapMatrix).

LaTeX

$$$$ |G.ConnectedComponent| = \\operatorname{finrank}_{\\mathbb{R}} \\ker\\bigl( \\mathrm{Matrix.toLin'}(G.lapMatrix \\mathbb{R}) \\bigr). $$$$

Lean4

/-- The number of connected components in `G` is the dimension of the nullspace of its Laplacian. -/
theorem card_connectedComponent_eq_finrank_ker_toLin'_lapMatrix :
    Fintype.card G.ConnectedComponent = Module.finrank ℝ (LinearMap.ker (Matrix.toLin' (G.lapMatrix ℝ))) := by
  classical rw [Module.finrank_eq_card_basis (lapMatrix_ker_basis G)]

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