Commit 2023-06-10 05:39 9b8201dd

View on Github →

feat: port LinearAlgebra.Matrix.Charpoly.Eigs (#4936)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Matrix/Charpoly/Eigs.lean

added theorem Matrix.det_eq_prod_roots_charpoly

added theorem Matrix.det_eq_prod_roots_charpoly_of_splits

added theorem Matrix.trace_eq_sum_roots_charpoly

added theorem Matrix.trace_eq_sum_roots_charpoly_of_splits