conj_eigenvalue_eq_self — Mathlib

English

If T is self-adjoint, then every eigenvalue of T is a real number.

Русский

Если T самосопряжённый, то каждый собственный показатель T является вещественным числом.

LaTeX

$$$$ \text{If } T \text{ is self-adjoint, then } \forall \mu \text{ with } T v=\mu v, \; \mu\in\mathbb{R}. $$$$

Lean4

/-- The eigenvalues of a self-adjoint operator are real. -/
theorem conj_eigenvalue_eq_self (hT : T.IsSymmetric) {μ : 𝕜} (hμ : HasEigenvalue T μ) : conj μ = μ :=
  by
  obtain ⟨v, hv₁, hv₂⟩ := hμ.exists_hasEigenvector
  rw [mem_eigenspace_iff] at hv₁
  simpa [hv₂, inner_smul_left, inner_smul_right, hv₁] using hT v v

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