Commit 2023-05-23 07:30 c0924978

View on Github →

feat: port LinearAlgebra.Charpoly.Basic (#4251)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Charpoly/Basic.lean

added theorem LinearMap.aeval_eq_aeval_mod_charpoly

added theorem LinearMap.aeval_self_charpoly

added def LinearMap.charpoly

added theorem LinearMap.charpoly_def

added theorem LinearMap.charpoly_monic

added theorem LinearMap.isIntegral

added theorem LinearMap.minpoly_coeff_zero_of_injective

added theorem LinearMap.minpoly_dvd_charpoly

added theorem LinearMap.pow_eq_aeval_mod_charpoly