# mathlibdocumentation

linear_algebra.matrix.charpoly.minpoly

# The minimal polynomial divides the characteristic polynomial of a matrix. #

theorem matrix.is_integral {R : Type u} [comm_ring R] {n : Type v} [decidable_eq n] [fintype n] {M : n R} :
M
theorem matrix.minpoly_dvd_charpoly {n : Type v} [decidable_eq n] [fintype n] {K : Type u_1} [field K] (M : n K) :
theorem charpoly_left_mul_matrix {K : Type u_1} {S : Type u_2} [field K] [comm_ring S] [ S] (h : S) :

The characteristic polynomial of the map λ x, a * x is the minimal polynomial of a.

In combination with det_eq_sign_charpoly_coeff or trace_eq_neg_charpoly_coeff and a bit of rewriting, this will allow us to conclude the field norm resp. trace of x is the product resp. sum of x's conjugates.