mathlib

b62dd289 - feat(linear_algebra/eigenspace): beginning to relate minimal polynomials to eigenvalues (#4165)

feat(linear_algebra/eigenspace): beginning to relate minimal polynomials to eigenvalues (#4165) rephrases some lemmas in `linear_algebra` to use `aeval` instead of `eval2` and `algebra_map` shows that an eigenvalue of a linear transformation is a root of its minimal polynomial, and vice versa