Theorem Matrix.det_eq_prod_roots_charpoly_of_splits

Modification history

2025-11-20 19:42
Mathlib/LinearAlgebra/Matrix/Charpoly/Eigs.lean
feat(Algebra/Polynomial/Splits): remove the `RingHom` argument of `Splits` (#31631)
Modified Matrix.det_eq_prod_roots_charpoly_of_splitsView on Github →
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 →