Documentation

Mathlib.LinearAlgebra.Charpoly.Basic

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 #

def LinearMap.charpoly {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] (f : M →ₗ[R] M) :

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

Equations
Instances For

    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} [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] (f : M →ₗ[R] M) :

    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} [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] (f : M →ₗ[R] M) (k : ) :
    f ^ k = ↑(Polynomial.aeval f) (Polynomial.X ^ k %ₘ LinearMap.charpoly f)

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