Theorem Matrix.mem_spectrum_of_isRoot_charpoly

Modification history

2025-10-09 18:05
Mathlib/LinearAlgebra/Matrix/Charpoly/Eigs.lean
feat(LinearAlgebra): roots of charpoly are the eigenvalues/spectrum (#29478)
Added Matrix.mem_spectrum_of_isRoot_charpolyView on Github →