eigenvectorBasis — Mathlib

English

There exists an orthonormal basis consisting of eigenvectors for a Hermitian matrix.

Русский

Существуют ортонормированные собственные векторы, образующие базис эрмитова матрицы.

LaTeX

$$$\text{IsHermitian}(A) \Rightarrow \text{there exists } \text{eigenvectorBasis} \text{ which is an orthonormal basis of eigenvectors.}$$$

Lean4

/-- A choice of an orthonormal basis of eigenvectors of a Hermitian matrix. -/
noncomputable def eigenvectorBasis : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n) :=
  ((isHermitian_iff_isSymmetric.1 hA).eigenvectorBasis finrank_euclideanSpace).reindex
    (Fintype.equivOfCardEq (Fintype.card_fin _))

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