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 →