# Eigenvalues are characteristic polynomial roots. #

In fields we show that:

`Matrix.det_eq_prod_roots_charpoly_of_splits`

: the determinant (in the field of the matrix) is the product of the roots of the characteristic polynomial if the polynomial splits in the field of the matrix.`Matrix.trace_eq_sum_roots_charpoly_of_splits`

: the trace is the sum of the roots of the characteristic polynomial if the polynomial splits in the field of the matrix.

In an algebraically closed field we show that:

`Matrix.det_eq_prod_roots_charpoly`

: the determinant is the product of the roots of the characteristic polynomial.`Matrix.trace_eq_sum_roots_charpoly`

: the trace is the sum of the roots of the characteristic polynomial.

Note that over other fields such as `ℝ`

, these results can be used by using
`A.map (algebraMap ℝ ℂ)`

as the matrix, and then applying `RingHom.map_det`

.

The two lemmas `Matrix.det_eq_prod_roots_charpoly`

and `Matrix.trace_eq_sum_roots_charpoly`

are more
commonly stated as trace is the sum of eigenvalues and determinant is the product of eigenvalues.
Mathlib has already defined eigenvalues in `LinearAlgebra.Eigenspace`

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.

## TODO #

The proofs of `det_eq_prod_roots_charpoly_of_splits`

and
`trace_eq_sum_roots_charpoly_of_splits`

closely resemble
`norm_gen_eq_prod_roots`

and `trace_gen_eq_sum_roots`

respectively, but the
dependencies are not general enough to unify them. We should refactor
`Polynomial.prod_roots_eq_coeff_zero_of_monic_of_split`

and
`Polynomial.sum_roots_eq_nextCoeff_of_monic_of_split`

to assume splitting over an arbitrary map.