English
Eigenvectors corresponding to distinct eigenvalues of a linear operator are linearly independent, indexed by a set with injective eigenvalues.
Русский
Собственные векторы, соответствующие различным собственным значениям линейного оператора, линейно независимы; индексируется по множеству собственных значений с различными значениями.
LaTeX
$$$\\text{Distinct eigenvalues yield linearly independent eigenvectors: }\\text{If } \\mu_i \\neq \\mu_j,\\; v_i, v_j \\text{ eigenvectors with eigenvalues } \\mu_i, \\mu_j, \\text{ then } \\{v_i\\}_{i}\\text{ is independent.}$$$
Lean4
/-- Eigenvectors corresponding to distinct eigenvalues of a linear operator are linearly
independent. (Lemma 5.10 of [axler2015])
We use the eigenvalues as indexing set to ensure that there is only one eigenvector for each
eigenvalue in the image of `xs`.
See `Module.End.eigenvectors_linearIndependent'` for an indexed variant. -/
theorem eigenvectors_linearIndependent [NoZeroSMulDivisors R M] (f : End R M) (μs : Set R) (xs : μs → M)
(h_eigenvec : ∀ μ : μs, f.HasEigenvector μ (xs μ)) : LinearIndependent R xs :=
f.eigenvectors_linearIndependent' (fun μ : μs ↦ μ) Subtype.coe_injective _ h_eigenvec
