Commit 2023-05-21 13:02 542f2e56

View on Github →

feat: port LinearAlgebra.Matrix.Charpoly.Basic (#4118) Very few fixes were needed for this file!

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Matrix/Charpoly/Basic.lean

added theorem Matrix.aeval_self_charpoly

added def Matrix.charpoly

added theorem Matrix.charpoly_reindex

added def charmatrix

added theorem charmatrix_apply

added theorem charmatrix_apply_eq

added theorem charmatrix_apply_ne

added theorem charmatrix_reindex

added theorem matPolyEquiv_charmatrix