eigenvectors_linearIndependent' — Mathlib

English

Eigenvectors corresponding to distinct eigenvalues of a linear operator are linearly independent.

Русский

Собственные векторы, соответствующие различным собственным значениям линейного оператора, линейно независимы.

LaTeX

$$$\\text{Eigenvectors corresponding to distinct eigenvalues are linearly independent.}$$$

Lean4

/-- Eigenvectors corresponding to distinct eigenvalues of a linear operator are linearly
independent. -/
theorem eigenvectors_linearIndependent' {ι : Type*} [NoZeroSMulDivisors R M] (f : End R M) (μ : ι → R)
    (hμ : Function.Injective μ) (v : ι → M) (h_eigenvec : ∀ i, f.HasEigenvector (μ i) (v i)) : LinearIndependent R v :=
  f.eigenspaces_iSupIndep.comp hμ |>.linearIndependent _ (fun i ↦ h_eigenvec i |>.left) (fun i ↦ h_eigenvec i |>.right)

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