Commit 2021-06-09 06:11 34c433d9

View on Github →

feat(data/finsupp): generalize finsupp.has_scalar to require only distrib_mul_action instead of semimodule (#7819) This propagates the generalization to (add_)monoid_algebra and mv_polynomial.

Estimated changes

Modified src/algebra/monoid_algebra.lean

Modified src/data/finsupp/basic.lean

modified theorem finsupp.coe_smul

modified theorem finsupp.filter_smul

modified theorem finsupp.map_domain_smul

modified theorem finsupp.map_range_smul

modified theorem finsupp.smul_apply

modified theorem finsupp.smul_single

modified theorem finsupp.sum_smul_index'

modified theorem finsupp.support_smul

Modified src/data/finsupp/to_dfinsupp.lean

modified theorem dfinsupp.to_finsupp_smul

modified theorem finsupp.to_dfinsupp_smul

Modified src/data/mv_polynomial/basic.lean

modified theorem mv_polynomial.coeff_smul