Theorem Matrix.det_eq_prod_roots_charpoly_of_splits

Modification history

2025-10-09 18:05
Mathlib/LinearAlgebra/Matrix/Charpoly/Eigs.lean
feat(LinearAlgebra): roots of charpoly are the eigenvalues/spectrum (#29478)
Modified Matrix.det_eq_prod_roots_charpoly_of_splitsView on Github →
2023-06-10 05:39
Mathlib/LinearAlgebra/Matrix/Charpoly/Eigs.lean
feat: port LinearAlgebra.Matrix.Charpoly.Eigs (#4936)
Added Matrix.det_eq_prod_roots_charpoly_of_splitsView on Github →