hasEigenvalue_eigenvalues — Mathlib

English

There exists an eigenvalue corresponding to every eigenvector in the eigenbasis.

Русский

Существуют собственные значения для каждого собственнического вектора базиса.

LaTeX

$$$$ \text{For each } i, \; \text{HasEigenvalue}(T, \lambda_i). $$$$

Lean4

theorem hasEigenvalue_eigenvalues (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (i : Fin n) :
    HasEigenvalue T (hT.eigenvalues hn i) :=
  Module.End.hasEigenvalue_of_hasEigenvector (hT.hasEigenvector_eigenvectorBasis hn i)

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