The minimal polynomial divides the characteristic polynomial of a matrix.

This also includes some miscellaneous results about minpoly on matrices.

@[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

@[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

theorem Matrix.isIntegral {R : Type u} [CommRing R] {n : Type v} [DecidableEq n] [Fintype n] (M : Matrix n n R) : IsIntegral R M

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

@[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

@[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

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.