hasEigenvalue_toLin'_diagonal_iff

English

An eigenvalue μ for the diagonal operator equals if and only if there exists i with d_i = μ.

Русский

Собственное значение μ для диагонального оператора существует тогда и только тогда, когда существует i такое, что d_i = μ.

LaTeX

$$$\\text{HasEigenvalue}((\\text{toLin'}(\\text{diagonal } d)), μ) \\iff \\exists i, d_i = μ$$$

Lean4

/-- Eigenvalues of a diagonal linear operator with respect to standard basis
are the diagonal entries. -/
theorem hasEigenvalue_toLin'_diagonal_iff [NoZeroDivisors R] (d : n → R) {μ : R} :
    HasEigenvalue (toLin' (diagonal d)) μ ↔ (∃ i, d i = μ) :=
  hasEigenvalue_toLin_diagonal_iff _ <| Pi.basisFun R n

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