# Characteristic polynomial #

We define the characteristic polynomial of f : M →ₗ[R] M, where M is a finite and free R-module. The proof that f.charpoly is the characteristic polynomial of the matrix of f in any basis is in LinearAlgebra/Charpoly/ToMatrix.

## Main definition #

• LinearMap.charpoly f : the characteristic polynomial of f : M →ₗ[R] M.
def LinearMap.charpoly {R : Type u} {M : Type v} [] [] [Module R M] [] [] (f : M →ₗ[R] M) :

The characteristic polynomial of f : M →ₗ[R] M.

Equations
• f.charpoly = (() f).charpoly
Instances For
theorem LinearMap.charpoly_def {R : Type u} {M : Type v} [] [] [Module R M] [] [] (f : M →ₗ[R] M) :
f.charpoly = (() f).charpoly
theorem LinearMap.charpoly_monic {R : Type u} {M : Type v} [] [] [Module R M] [] [] (f : M →ₗ[R] M) :
f.charpoly.Monic
theorem LinearMap.charpoly_natDegree {R : Type u} {M : Type v} [] [] [] [Module R M] [] [] (f : M →ₗ[R] M) :
f.charpoly.natDegree =
theorem LinearMap.aeval_self_charpoly {R : Type u} {M : Type v} [] [] [Module R M] [] [] (f : M →ₗ[R] M) :
() f.charpoly = 0

The Cayley-Hamilton Theorem, that the characteristic polynomial of a linear map, applied to the linear map itself, is zero.

See Matrix.aeval_self_charpoly for the equivalent statement about matrices.

theorem LinearMap.isIntegral {R : Type u} {M : Type v} [] [] [Module R M] [] [] (f : M →ₗ[R] M) :
theorem LinearMap.minpoly_dvd_charpoly {K : Type u} {M : Type v} [] [] [Module K M] [] (f : M →ₗ[K] M) :
minpoly K f f.charpoly
theorem LinearMap.aeval_eq_aeval_mod_charpoly {R : Type u} {M : Type v} [] [] [Module R M] [] [] (f : M →ₗ[R] M) (p : ) :
() p = () (p %ₘ f.charpoly)

Any endomorphism polynomial p is equivalent under evaluation to p %ₘ f.charpoly; that is, p is equivalent to a polynomial with degree less than the dimension of the module.

theorem LinearMap.pow_eq_aeval_mod_charpoly {R : Type u} {M : Type v} [] [] [Module R M] [] [] (f : M →ₗ[R] M) (k : ) :
f ^ k = () (Polynomial.X ^ k %ₘ f.charpoly)

Any endomorphism power can be computed as the sum of endomorphism powers less than the dimension of the module.

theorem LinearMap.minpoly_coeff_zero_of_injective {R : Type u} {M : Type v} [] [] [] [Module R M] [] [] {f : M →ₗ[R] M} (hf : ) :
(minpoly R f).coeff 0 0