hasEigenvector_eigenvectorBasis — Mathlib

English

For each i, there exists a vector that is an eigenvector corresponding to the i-th eigenvalue, forming the eigenvector basis.

Русский

Для каждого индекса i существует собственный вектор, соответствующий i-тому собственному значению, образующий базис собственных векторов.

LaTeX

$$$$ \exists v_i \neq 0: T v_i = \lambda_i v_i \text{ with } \{v_i\} \text{ forming a basis}. $$$$

Lean4

theorem hasEigenvector_eigenvectorBasis (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (i : Fin n) :
    HasEigenvector T (hT.eigenvalues hn i) (hT.eigenvectorBasis hn i) :=
  by
  rw [eigenvalues_def, eigenvectorBasis_def, OrthonormalBasis.reindex_apply]
  apply hasEigenvector_eigenvectorBasis_helper

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