Commit 2023-05-23 11:05 7e279c7e

View on Github →

feat: port LinearAlgebra.Matrix.Charpoly.Minpoly (#4266)

Estimated changes

Modified Mathlib.lean

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

added theorem LinearMap.minpoly_toMatrix'

added theorem LinearMap.minpoly_toMatrix

added theorem Matrix.isIntegral

added theorem Matrix.minpoly_dvd_charpoly

added theorem Matrix.minpoly_toLin'

added theorem Matrix.minpoly_toLin

added theorem charpoly_leftMulMatrix