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
matrix/charpoly/coeff for corollaries of this theorem.
Main definitions #
matrix.charpolyis the characteristic polynomial of a matrix.
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.
- charmatrix M = ⇑(matrix.scalar n) polynomial.X - ⇑(polynomial.C.map_matrix) M
The characteristic polynomial of a matrix
M is given by $\det (t I - M)$.
- M.charpoly = (charmatrix M).det
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.