Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-17 19:11 9745b093

View on Github →

feat(linear_algebra/matrix/charpoly): Coefficients of the characteristic polynomial falls in the ideal power. (#15459)

Estimated changes

Modified src/algebra/order/sub.lean

added theorem add_tsub_add_le_tsub_add_tsub

Modified src/linear_algebra/matrix/charpoly/basic.lean

added theorem charmatrix_apply

Modified src/linear_algebra/matrix/charpoly/coeff.lean

added theorem coeff_charpoly_mem_ideal_pow

Modified src/ring_theory/polynomial/basic.lean

added theorem polynomial.coeff_prod_mem_ideal_pow_tsub