Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-01 08:30 8f78eb9c

View on Github →

feat(*): generalize to and add distrib_smul instances (#16132) This PR builds on #16123 by adding distrib_smul (and smul_zero_class) instances for:

  • finsupp
  • add_monoid_algebra
  • polynomial
  • submodule quotients
  • scalar multiplication by ℚ It also generalizes some results by weakening distrib_mul_action to distrib_smul. The choice of instances and generalizations is based on which are necessary to solve instance diamonds in splitting_field, so I probably missed a lot of additional changes. Since I'm not so interested in generalizing everything at the moment, I'd rather leave missing instances to follow-up PRs.

Estimated changes

modified theorem finsupp.coe_smul
modified theorem finsupp.smul_apply
modified theorem finsupp.sum_smul_index'
modified theorem is_smul_regular.finsupp
modified theorem polynomial.of_finsupp_smul
modified theorem polynomial.to_finsupp_smul
modified theorem smul_add
modified theorem smul_zero