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

This also includes some miscellaneous results about `minpoly` on matrices.

source
@[simp]
theorem Matrix.minpoly_toLin' {R : Type u} [CommRing R] {n : Type v} [DecidableEq n] [Fintype n] (M : Matrix n n R) :
minpoly R (toLin' M) = minpoly R M
source
@[simp]
theorem Matrix.minpoly_toLin {R : Type u} [CommRing R] {n : Type v} [DecidableEq n] [Fintype n] {N : Type w} [AddCommGroup N] [Module R N] (b : Module.Basis n R N) (M : Matrix n n R) :
minpoly R ((toLin b b) M) = minpoly R M
source
theorem Matrix.isIntegral {R : Type u} [CommRing R] {n : Type v} [DecidableEq n] [Fintype n] (M : Matrix n n R) :
IsIntegral R M
source
theorem Matrix.minpoly_dvd_charpoly {n : Type v} [DecidableEq n] [Fintype n] {K : Type u_1} [Field K] (M : Matrix n n K) :
minpoly K M ∣ M.charpoly
source
@[simp]
theorem LinearMap.minpoly_toMatrix' {R : Type u} [CommRing R] {n : Type v} [DecidableEq n] [Fintype n] (f : (n → R) →ₗ[R] n → R) :
minpoly R (toMatrix' f) = minpoly R f
source
@[simp]
theorem LinearMap.minpoly_toMatrix {R : Type u} [CommRing R] {n : Type v} [DecidableEq n] [Fintype n] {N : Type w} [AddCommGroup N] [Module R N] (b : Module.Basis n R N) (f : N →ₗ[R] N) :
minpoly R ((toMatrix b b) f) = minpoly R f
source
theorem charpoly_leftMulMatrix {R : Type u} [CommRing R] {S : Type u_1} [Ring S] [Algebra R S] (h : PowerBasis R S) :
((Algebra.leftMulMatrix h.basis) h.gen).charpoly = minpoly R h.gen

The characteristic polynomial of the map `fun 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.