Mathlib v3 is deprecated. Go to Mathlib v4

Theorem linear_map.minpoly_to_matrix

Modification history

2023-05-19 07:37

src/linear_algebra/matrix/charpoly/minpoly.lean

feat(linear_algebra/matrix/charpoly/minpoly): `minpoly` is unaffected by `to_lin` and `to_matrix` (#19036)

Added linear_map.minpoly_to_matrix View on Github →