# mathlib3documentation

linear_algebra.matrix.charpoly.minpoly

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This also includes some miscellaneous results about minpoly on matrices.

@[simp]
theorem matrix.minpoly_to_lin' {R : Type u} [comm_ring R] {n : Type v} [decidable_eq n] [fintype n] (M : n R) :
= M
@[simp]
theorem matrix.minpoly_to_lin {R : Type u} [comm_ring R] {n : Type v} [decidable_eq n] [fintype n] {N : Type w} [ N] (b : R N) (M : n R) :
( b) M) = M
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) :
@[simp]
theorem linear_map.minpoly_to_matrix' {R : Type u} [comm_ring R] {n : Type v} [decidable_eq n] [fintype n] (f : (n R) →ₗ[R] n R) :
= f
@[simp]
theorem linear_map.minpoly_to_matrix {R : Type u} [comm_ring R] {n : Type v} [decidable_eq n] [fintype n] {N : Type w} [ N] (b : R N) (f : N →ₗ[R] N) :
( b) f) = f
theorem charpoly_left_mul_matrix {R : Type u} [comm_ring R] {S : Type u_1} [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.