English
The family (lapMatrix_ker_basis_aux G) indexed by the connected components of G is linearly independent over ℝ. In other words, the vectors corresponding to different components are independent.
Русский
Множество (lapMatrix_ker_basis_aux G), индексируемое по связным компонентам G, линейно независимо над ℝ. Векторные базисы, соответствующие разные компоненты, независимы.
LaTeX
$$$$ \\text{LinearIndependent}_{\\mathbb{R}}\\bigl( \\{ \\mathrm{lapMatrix\_ker\_basis\_aux}(G)(c) \\mid c \\in G.ConnectedComponent \\} \\bigr). $$$$
Lean4
theorem linearIndependent_lapMatrix_ker_basis_aux : LinearIndependent ℝ (lapMatrix_ker_basis_aux G) :=
by
rw [Fintype.linearIndependent_iff]
intro g h0
rw [Subtype.ext_iff] at h0
have h : ∑ c, g c • lapMatrix_ker_basis_aux G c = fun i ↦ g (connectedComponentMk G i) :=
by
simp only [lapMatrix_ker_basis_aux, SetLike.mk_smul_mk]
repeat rw [AddSubmonoid.coe_finset_sum]
ext i
simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul, mul_ite, mul_one, mul_zero, sum_ite_eq, mem_univ,
↓reduceIte]
rw [h] at h0
intro c
obtain ⟨i, h'⟩ : ∃ i : V, G.connectedComponentMk i = c := Quot.exists_rep c
exact h' ▸ congrFun h0 i
