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