# 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 Matrix.charmatrix {R : Type u_1} [] {n : Type u_4} [] [] (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.

Equations
• M.charmatrix = () Polynomial.X - Polynomial.C.mapMatrix M
Instances For
theorem Matrix.charmatrix_apply {R : Type u_1} [] {n : Type u_4} [] [] (M : Matrix n n R) (i : n) (j : n) :
M.charmatrix i j = Matrix.diagonal (fun (x : n) => Polynomial.X) i j - Polynomial.C (M i j)
@[simp]
theorem Matrix.charmatrix_apply_eq {R : Type u_1} [] {n : Type u_4} [] [] (M : Matrix n n R) (i : n) :
M.charmatrix i i = Polynomial.X - Polynomial.C (M i i)
@[simp]
theorem Matrix.charmatrix_apply_ne {R : Type u_1} [] {n : Type u_4} [] [] (M : Matrix n n R) (i : n) (j : n) (h : i j) :
M.charmatrix i j = -Polynomial.C (M i j)
theorem Matrix.matPolyEquiv_charmatrix {R : Type u_1} [] {n : Type u_4} [] [] (M : Matrix n n R) :
matPolyEquiv M.charmatrix = Polynomial.X - Polynomial.C M
theorem Matrix.charmatrix_reindex {R : Type u_1} [] {m : Type u_3} {n : Type u_4} [] [] [] [] (M : Matrix n n R) (e : n m) :
(() M).charmatrix = () M.charmatrix
theorem Matrix.charmatrix_map {R : Type u_1} {S : Type u_2} [] [] {n : Type u_4} [] [] (M : Matrix n n R) (f : R →+* S) :
(M.map f).charmatrix = M.charmatrix.map ()
theorem Matrix.charmatrix_fromBlocks {R : Type u_1} [] {m : Type u_3} {n : Type u_4} [] [] [] [] (M₁₁ : Matrix m m R) (M₁₂ : Matrix m n R) (M₂₁ : Matrix n m R) (M₂₂ : Matrix n n R) :
(Matrix.fromBlocks M₁₁ M₁₂ M₂₁ M₂₂).charmatrix = Matrix.fromBlocks M₁₁.charmatrix (-M₁₂.map Polynomial.C) (-M₂₁.map Polynomial.C) M₂₂.charmatrix
def Matrix.charpoly {R : Type u_1} [] {n : Type u_4} [] [] (M : Matrix n n R) :

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

Equations
• M.charpoly = M.charmatrix.det
Instances For
theorem Matrix.charpoly_reindex {R : Type u_1} [] {m : Type u_3} {n : Type u_4} [] [] [] [] (e : n m) (M : Matrix n n R) :
(() M).charpoly = M.charpoly
theorem Matrix.charpoly_map {R : Type u_1} {S : Type u_2} [] [] {n : Type u_4} [] [] (M : Matrix n n R) (f : R →+* S) :
(M.map f).charpoly = Polynomial.map f M.charpoly
@[simp]
theorem Matrix.charpoly_fromBlocks_zero₁₂ {R : Type u_1} [] {m : Type u_3} {n : Type u_4} [] [] [] [] (M₁₁ : Matrix m m R) (M₂₁ : Matrix n m R) (M₂₂ : Matrix n n R) :
(Matrix.fromBlocks M₁₁ 0 M₂₁ M₂₂).charpoly = M₁₁.charpoly * M₂₂.charpoly
@[simp]
theorem Matrix.charpoly_fromBlocks_zero₂₁ {R : Type u_1} [] {m : Type u_3} {n : Type u_4} [] [] [] [] (M₁₁ : Matrix m m R) (M₁₂ : Matrix m n R) (M₂₂ : Matrix n n R) :
(Matrix.fromBlocks M₁₁ M₁₂ 0 M₂₂).charpoly = M₁₁.charpoly * M₂₂.charpoly
theorem Matrix.aeval_self_charpoly {R : Type u_1} [] {n : Type u_4} [] [] (M : Matrix n n R) :
() M.charpoly = 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.