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 →