mathlib
34c433d9 - feat(data/finsupp): generalize finsupp.has_scalar to require only distrib_mul_action instead of semimodule (#7819)

Commit

4 years ago

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.

Author

eric-wieser

Parents

393f6389

mathlib 34c433d9 - feat(data/finsupp): generalize finsupp.has_scalar to require only distrib_mul_action instead of semimodule (#7819)

mathlib
34c433d9 - feat(data/finsupp): generalize finsupp.has_scalar to require only distrib_mul_action instead of semimodule (#7819)