eigenvalues_mem_spectrum_real — Mathlib

English

There is a unitary matrix whose columns are the eigenvectors of A.

Русский

Существует единичная унитарная матрица, столбцы которой являются собственными векторами A.

LaTeX

$$$\text{eigenvectorUnitary}(h_A) \text{ is a unitary matrix with columns equal to eigenvectors of } A$$$

Lean4

/-- Eigenvalues of a Hermitian matrix A are in the ℝ spectrum of A. -/
theorem eigenvalues_mem_spectrum_real (i : n) : hA.eigenvalues i ∈ spectrum ℝ A :=
  by
  apply spectrum.of_algebraMap_mem 𝕜
  rw [← Matrix.spectrum_toEuclideanLin]
  exact LinearMap.IsSymmetric.hasEigenvalue_eigenvalues _ _ _ |>.mem_spectrum

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