Theorem Matrix.mem_spectrum_of_isRoot_charpoly

Modification history

2026-05-23 12:03
Mathlib/LinearAlgebra/Matrix/Charpoly/Eigs.lean
feat(LinearAlgebra/Matrix/Charpoly/Eigs): generalize to `CommRing`s (#39601) …
Modified Matrix.mem_spectrum_of_isRoot_charpolyView on Github →
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 →