Commit 2020-09-05 09:19 364d5d4c
View on Github →feat(linear_algebra/char_poly): rephrase Cayley-Hamilton with aeval', define matrix.min_poly([#4040](https://github.com/leanprover-community/mathlib/pull/4040)) Rephrases the Cayley-Hamilton theorem to useaeval, renames it aeval_self_char_polyDefinesmatrix.min_poly, the minimal polynomial of a matrix, which divides char_poly`