Characteristic polynomials and the Cayley-Hamilton theorem #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
We define characteristic polynomials of matrices and
prove the Cayley–Hamilton theorem over arbitrary commutative rings.
See the file
matrix/charpoly/coeff for corollaries of this theorem.
Main definitions #
Implementation details #
We follow a nice proof from http://drorbn.net/AcademicPensieve/2015-12/CayleyHamilton.pdf
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.
The characteristic polynomial of a matrix
M is given by $\det (t I - M)$.
The Cayley-Hamilton Theorem, that the characteristic polynomial of a matrix,
applied to the matrix itself, is zero.
This holds over any commutative ring.
linear_map.aeval_self_charpoly for the equivalent statement about endomorphisms.