Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-23 00:38 20981bee

View on Github →

feat(linear_algebra/charpoly): add linear_map.charpoly (#9279) We add linear_map.charpoly, the characteristic polynomial of an endomorphism of a finite free module, and a basic API.

Estimated changes

Created src/linear_algebra/charpoly.lean

added theorem linear_map.aeval_self_charpoly

added def linear_map.charpoly

added theorem linear_map.charpoly_coeff_zero_of_injective

added theorem linear_map.charpoly_def

added theorem linear_map.charpoly_monic

added theorem linear_map.charpoly_to_matrix

added theorem linear_map.is_integral

added theorem linear_map.minpoly_dvd_charpoly

Modified src/linear_algebra/charpoly/basic.lean

added theorem charmatrix_reindex

added theorem matrix.charpoly_reindex

Modified src/linear_algebra/dimension.lean

added def basis.index_equiv

Modified src/linear_algebra/eigenspace.lean

Modified src/linear_algebra/free_module_pid.lean