apply_eigenvectorBasis — Mathlib

English

On an eigenvector, the operator acts by scalar multiplication by its eigenvalue.

Русский

На собственном векторе оператор действует умножением на собственное значение.

LaTeX

$$$$ T(v_i) = \lambda_i v_i, \; v_i \in \mathrm{Eig}(T, \lambda_i). $$$$

Lean4

@[simp]
theorem apply_eigenvectorBasis (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (i : Fin n) :
    T (hT.eigenvectorBasis hn i) = (hT.eigenvalues hn i : 𝕜) • hT.eigenvectorBasis hn i :=
  mem_eigenspace_iff.mp (hT.hasEigenvector_eigenvectorBasis hn i).1

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