# mathlibdocumentation

linear_algebra.char_poly.basic

# Characteristic polynomials and the Cayley-Hamilton theorem

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

## Main definitions

• char_poly is the characteristic polynomial of a matrix.

## Implementation details

def char_matrix {R : Type u} [comm_ring R] {n : Type w} [decidable_eq n] [fintype n] (M : n R) :
n (polynomial R)

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
@[simp]
theorem char_matrix_apply_eq {R : Type u} [comm_ring R] {n : Type w} [decidable_eq n] [fintype n] (M : n R) (i : n) :

@[simp]
theorem char_matrix_apply_ne {R : Type u} [comm_ring R] {n : Type w} [decidable_eq n] [fintype n] (M : n R) (i j : n) (h : i j) :
i j = -polynomial.C (M i j)

theorem mat_poly_equiv_char_matrix {R : Type u} [comm_ring R] {n : Type w} [decidable_eq n] [fintype n] (M : n R) :

def char_poly {R : Type u} [comm_ring R] {n : Type w} [decidable_eq n] [fintype n] (M : n R) :

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

Equations
theorem aeval_self_char_poly {R : Type u} [comm_ring R] {n : Type w} [decidable_eq n] [fintype n] (M : n R) :
(char_poly M) = 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.