Commit 2023-05-21 21:36 b37b871d

View on Github →

feat: port LinearAlgebra.Matrix.Charpoly.LinearMap (#4172)

Estimated changes

Modified Mathlib.lean

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

added theorem LinearMap.exists_monic_and_aeval_eq_zero

added theorem LinearMap.exists_monic_and_coeff_mem_pow_and_aeval_eq_zero_of_range_le_smul

added theorem Matrix.Represents.add

added theorem Matrix.Represents.congr_fun

added theorem Matrix.Represents.eq

added theorem Matrix.Represents.mul

added theorem Matrix.Represents.one

added theorem Matrix.Represents.smul

added theorem Matrix.Represents.zero

added def Matrix.Represents

added theorem Matrix.isRepresentation.eq_toEnd_of_represents

added theorem Matrix.isRepresentation.toEnd_exists_mem_ideal

added theorem Matrix.isRepresentation.toEnd_represents

added theorem Matrix.isRepresentation.toEnd_surjective

added def Matrix.isRepresentation

added theorem Matrix.represents_iff'

added theorem Matrix.represents_iff

added def PiToModule.fromEnd

added theorem PiToModule.fromEnd_apply

added theorem PiToModule.fromEnd_apply_single_one

added theorem PiToModule.fromEnd_injective

added def PiToModule.fromMatrix

added theorem PiToModule.fromMatrix_apply

added theorem PiToModule.fromMatrix_apply_single_one