mathlib

48dc6abe - feat(linear_algebra/matrix/charpoly/eigs): det and trace are product and sum of eigenvalues (#19079)

feat(linear_algebra/matrix/charpoly/eigs): det and trace are product and sum of eigenvalues (#19079) This adds two lemmas: 1. `det_eq_prod_roots_charpoly`: the determinant of a square matrix is the product of the characteristic polynomial roots of that matrix. 2. `trace_eq_sum_roots_charpoly`: the trace is similarly the sum of the characteristic polynomial roots. These two lemmas are more commonly stated as trace is the sum of eigenvalues and determinant is the product of eigenvalues. Mathlib has already defined eigenvalues in [linear_algebra.eigenspace](https://leanprover-community.github.io/mathlib_docs/linear_algebra/eigenspace.html#module.End.eigenvalues) as the roots of the minimal polynomial of a linear endomorphism. These do not have correct multiplicity and cannot be used in the theorems above. Hence we express these theorems in terms of the roots of the characteristic polynomial directly. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>