mathlib documentation


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 : matrix n n R} :
theorem matrix.minpoly_dvd_charpoly {n : Type v} [decidable_eq n] [fintype n] {K : Type u_1} [field K] (M : matrix n n K) :
theorem charpoly_left_mul_matrix {R : Type u} [comm_ring R] {S : Type u_1} [ring S] [algebra R S] (h : power_basis R 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.