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]
{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)
:
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 ∣ Matrix.charpoly M
@[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)
:
minpoly R (↑(LinearMap.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)
:
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.