Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-07 01:12 ef7c3350

View on Github →

fix(data/mv_polynomial): add missing decidable arguments (#7817) This:

  • fixes a doubled instance name, finsupp.finsupp.decidable_eq. Note the linter deliberate ignores instances, as they are often autogenerated
  • generalizes finsupp.decidable_le to all canonically_ordered_monoids
  • adds missing decidable_eq arguments to mv_polynomial and mv_power_series lemmas whose statement contains an if. These might in future be lintable.
  • adds some missing lemmas about mv_polynomial to clean up a few proofs.

Estimated changes

modified theorem mv_polynomial.coeff_C
modified theorem mv_polynomial.coeff_X'
modified theorem mv_polynomial.coeff_X_pow
modified theorem mv_polynomial.coeff_mul_X'
modified theorem mv_polynomial.pderiv_X
modified theorem mv_power_series.coeff_C
modified theorem mv_power_series.coeff_X
modified theorem mv_power_series.coeff_X_pow
modified theorem mv_power_series.coeff_inv
modified theorem mv_power_series.coeff_one
modified theorem power_series.coeff_zero_C
modified theorem power_series.coeff_zero_X
modified theorem power_series.order_monomial