Commit 2023-09-04 13:18 351431b2

View on Github →

feat: nilpotent matrices have nilpotent trace (#6588) Also some related results

Estimated changes

Modified Mathlib/Algebra/GeomSum.lean

added theorem Commute.sub_dvd_pow_sub_pow

added theorem one_sub_dvd_one_sub_pow

added theorem sub_one_dvd_pow_sub_one

Modified Mathlib/Data/Fintype/Card.lean

Modified Mathlib/Data/Polynomial/Basic.lean

added theorem Polynomial.coeff_one

Modified Mathlib/Data/Polynomial/Coeff.lean

deleted theorem Polynomial.coeff_one

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

added def Matrix.charpolyRev

modified theorem Matrix.charpoly_natDegree_eq_dim

added theorem Matrix.coeff_charpolyRev_eq_neg_trace

added theorem Matrix.eval_charpolyRev

added theorem Matrix.isNilpotent_charpoly_sub_pow_of_isNilpotent

added theorem Matrix.isNilpotent_trace_of_isNilpotent

added theorem Matrix.isUnit_charpolyRev_of_IsNilpotent

modified theorem Matrix.reverse_charpoly

Modified Mathlib/LinearAlgebra/Matrix/Charpoly/FiniteField.lean

Modified Mathlib/LinearAlgebra/Matrix/Trace.lean

added theorem Matrix.trace_eq_zero_of_isEmpty

Modified Mathlib/RingTheory/Polynomial/Nilpotent.lean

added theorem Polynomial.isNilpotent_reflect_iff

Modified Mathlib/RingTheory/PowerSeries/Basic.lean

Modified test/ComputeDegree.lean