# 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.

theorem Matrix.det_eq_prod_roots_charpoly_of_splits {n : Type u_1} [] [] {R : Type u_2} [] {A : Matrix n n R} (hAps : Polynomial.Splits () A.charpoly) :
A.det = A.charpoly.roots.prod
theorem Matrix.trace_eq_sum_roots_charpoly_of_splits {n : Type u_1} [] [] {R : Type u_2} [] {A : Matrix n n R} (hAps : Polynomial.Splits () A.charpoly) :
A.trace = A.charpoly.roots.sum
theorem Matrix.det_eq_prod_roots_charpoly {n : Type u_1} [] [] {R : Type u_2} [] (A : Matrix n n R) [] :
A.det = A.charpoly.roots.prod
theorem Matrix.trace_eq_sum_roots_charpoly {n : Type u_1} [] [] {R : Type u_2} [] (A : Matrix n n R) [] :
A.trace = A.charpoly.roots.sum