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} [CommRing R] {n : Type v} [DecidableEq n] [Fintype n] (M : Matrix n n R) :
minpoly R (Matrix.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 : Basis n R N) (M : Matrix n n R) :
minpoly R ((Matrix.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) :
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 : (nR) →ₗ[R] nR) :
minpoly R (LinearMap.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 : Basis n R N) (f : N →ₗ[R] N) :
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.