English
There exists a basis for ker(Matrix.toLin'(G.lapMatrix ℝ)) indexed by G.ConnectedComponent, consisting of functions that are 1 on a component and 0 elsewhere.
Русский
Существует база для ядра ker(Matrix.toLin'(G.lapMatrix ℝ)), индексируемая по G.ConnectedComponent, состоящая из функций, равных 1 на компоненте и 0 в остальных местах.
LaTeX
$$$$ \\mathrm{lapMatrix\\_ker\\_basis} G \\text{ is a basis of } \\ker(\\mathrm{Matrix.toLin'}(G.lapMatrix \\mathbb{R})). $$$$
Lean4
/-- `lapMatrix_ker_basis G` is a basis of the nullspace indexed by its connected components,
the basis is made up of the functions `V → ℝ` which are `1` on the vertices of the given
connected component and `0` elsewhere. -/
noncomputable def lapMatrix_ker_basis :=
Basis.mk (linearIndependent_lapMatrix_ker_basis_aux G) (top_le_span_range_lapMatrix_ker_basis_aux G)
