# Documentation

Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly

# 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} [] {n : Type v} [] [] (M : Matrix n n R) :
minpoly R (Matrix.toLin' M) = minpoly R M
@[simp]
theorem Matrix.minpoly_toLin {R : Type u} [] {n : Type v} [] [] {N : Type w} [] [Module R N] (b : Basis n R N) (M : Matrix n n R) :
minpoly R (↑() M) = minpoly R M
theorem Matrix.isIntegral {R : Type u} [] {n : Type v} [] [] (M : Matrix n n R) :
theorem Matrix.minpoly_dvd_charpoly {n : Type v} [] [] {K : Type u_1} [] (M : Matrix n n K) :
@[simp]
theorem LinearMap.minpoly_toMatrix' {R : Type u} [] {n : Type v} [] [] (f : (nR) →ₗ[R] nR) :
minpoly R (LinearMap.toMatrix' f) = minpoly R f
@[simp]
theorem LinearMap.minpoly_toMatrix {R : Type u} [] {n : Type v} [] [] {N : Type w} [] [Module R N] (b : Basis n R N) (f : N →ₗ[R] N) :
minpoly R (↑() f) = minpoly R f
theorem charpoly_leftMulMatrix {R : Type u} [] {S : Type u_1} [Ring S] [Algebra R S] (h : ) :
Matrix.charpoly (↑(Algebra.leftMulMatrix h.basis) h.gen) = 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.