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} :
is_integral R M
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
{K : Type u_1}
{S : Type u_2}
[field K]
[comm_ring S]
[algebra K S]
(h : power_basis K 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.