spectrum_eq_image_range — Mathlib

English

The spectrum of a Hermitian matrix is the image of its eigenvalues under the natural embedding of the real numbers into the base field.

Русский

Спектр эрмитовой матрицы есть образ её собственных значений под естественным вложением Реальных чисел в основание поля.

LaTeX

$$$\\\\operatorname{Spectrum}(A) = \\\\mathrm{ofReal}''\\\\mathrm{range}(h_A\\\\,\\\\mathrm{eigenvalues})$$$

Lean4

/-- The spectrum of a Hermitian matrix is the range of its eigenvalues under `RCLike.ofReal`. -/
theorem spectrum_eq_image_range : spectrum 𝕜 A = RCLike.ofReal '' Set.range hA.eigenvalues :=
  Set.ext fun x => by
    conv_lhs => rw [hA.spectral_theorem]
    simp

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