Theorem Matrix.det_eq_prod_roots_charpoly

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 View 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 View on Github →