Theorem hasEigenvector_toLin_diagonal

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 hasEigenvector_toLin_diagonalView on Github →