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_polyis 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.
The Cayley-Hamilton theorem, that the characteristic polynomial of a matrix, applied to the matrix itself, is zero.
This holds over any commutative ring.