Theorem hasEigenvalue_toLin_diagonal_iff

Modification history

2024-06-27 18:55
Mathlib/LinearAlgebra/Eigenspace/Matrix.lean
feat: the spectrum of a diagonal matrix is the range of the diagonal (#13837) …
Added hasEigenvalue_toLin_diagonal_iffView on Github →