# Documentation

Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

# Characteristic polynomials and the Cayley-Hamilton theorem #

We define characteristic polynomials of matrices and prove the Cayley–Hamilton theorem over arbitrary commutative rings.

See the file Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean for corollaries of this theorem.

## Main definitions #

• Matrix.charpoly is the characteristic polynomial of a matrix.

## Implementation details #

def charmatrix {R : Type u} [] {n : Type w} [] [] (M : Matrix n n R) :
Matrix n n ()

The "characteristic matrix" of M : Matrix n n R is the matrix of polynomials $t I - M$. The determinant of this matrix is the characteristic polynomial.

Instances For
theorem charmatrix_apply {R : Type u} [] {n : Type w} [] [] (M : Matrix n n R) (i : n) (j : n) :
charmatrix M i j = Polynomial.X * OfNat.ofNat 1 i j - Polynomial.C (M i j)
@[simp]
theorem charmatrix_apply_eq {R : Type u} [] {n : Type w} [] [] (M : Matrix n n R) (i : n) :
charmatrix M i i = Polynomial.X - Polynomial.C (M i i)
@[simp]
theorem charmatrix_apply_ne {R : Type u} [] {n : Type w} [] [] (M : Matrix n n R) (i : n) (j : n) (h : i j) :
charmatrix M i j = -Polynomial.C (M i j)
theorem matPolyEquiv_charmatrix {R : Type u} [] {n : Type w} [] [] (M : Matrix n n R) :
matPolyEquiv () = Polynomial.X - Polynomial.C M
theorem charmatrix_reindex {R : Type u} [] {n : Type w} [] [] {m : Type v} [] [] (e : n m) (M : Matrix n n R) :
charmatrix (↑() M) = ↑() ()
def Matrix.charpoly {R : Type u} [] {n : Type w} [] [] (M : Matrix n n R) :

The characteristic polynomial of a matrix M is given by $\det (t I - M)$.

Instances For
theorem Matrix.charpoly_reindex {R : Type u} [] {n : Type w} [] [] {m : Type v} [] [] (e : n m) (M : Matrix n n R) :
Matrix.charpoly (↑() M) =
theorem Matrix.aeval_self_charpoly {R : Type u} [] {n : Type w} [] [] (M : Matrix n n R) :
↑() () = 0

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

This holds over any commutative ring.

See LinearMap.aeval_self_charpoly for the equivalent statement about endomorphisms.