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