mathlib3

364d5d4c - feat(linear_algebra/char_poly): rephrase Cayley-Hamilton with `aeval', define `matrix.min_poly` (#4040)

feat(linear_algebra/char_poly): rephrase Cayley-Hamilton with `aeval', define `matrix.min_poly` (#4040) Rephrases the Cayley-Hamilton theorem to use `aeval`, renames it `aeval_self_char_poly` Defines `matrix.min_poly`, the minimal polynomial of a matrix, which divides `char_poly`