Commit 2023-05-21 17:21 a1ec3995

View on Github →

feat: port LinearAlgebra.Matrix.Charpoly.Coeff (#4169) Most of the file had minor fixes. I added porting notes for everything that was not just a capitalization issue. I tried to fix all the capitalization issues in the first actual commit (2492f1c1add83cbcf58705a03c6e1c22d5218eb9). The next commit (b59a8cf3d8863ddd882e27e0e28b97bd39d4c768) contains all the porting notes. I still have not managed to fix one of the proofs, though.

Estimated changes

Modified Mathlib.lean

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

added theorem Matrix.aeval_eq_aeval_mod_charpoly

added theorem Matrix.charpoly_coeff_eq_prod_coeff_of_le

added theorem Matrix.charpoly_degree_eq_dim

added theorem Matrix.charpoly_monic

added theorem Matrix.charpoly_natDegree_eq_dim

added theorem Matrix.charpoly_sub_diagonal_degree_lt

added theorem Matrix.det_eq_sign_charpoly_coeff

added theorem Matrix.det_of_card_zero

added theorem Matrix.eval_det

added theorem Matrix.matPolyEquiv_eval

added theorem Matrix.pow_eq_aeval_mod_charpoly

added theorem Matrix.trace_eq_neg_charpoly_coeff

added theorem charmatrix_apply_natDegree

added theorem charmatrix_apply_natDegree_le

added theorem coeff_charpoly_mem_ideal_pow

added theorem matPolyEquiv_eq_x_pow_sub_c