spectrum_diagonal — Mathlib

English

The spectrum of a diagonal operator equals the range of the diagonal entries.

Русский

Спектр диагонального оператора равен диапазону диагональных элементов.

LaTeX

$$$$ \operatorname{spec}_R(\operatorname{diag}(d)) = \mathrm{range}(d). $$$$

Lean4

/-- The spectrum of the diagonal operator is the range of the diagonal viewed as a function. -/
@[simp]
theorem spectrum_diagonal [Field R] (d : n → R) : spectrum R (diagonal d) = Set.range d :=
  by
  ext μ
  rw [← AlgEquiv.spectrum_eq (toLinAlgEquiv <| Pi.basisFun R n), ← hasEigenvalue_iff_mem_spectrum]
  exact hasEigenvalue_toLin'_diagonal_iff d

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