Add scalar multiplication for multisets.
The operation n *: X multiplies the multiplicity of each element x ∈ X with n
This MR:
- Introduces a type class
ScalarMul N A := N → A → Awith associated notations for scalar multiplication. The notation*:is taken from ssreflect, see https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/ssrnotations.v - Provides an instance
ScalarMul nat (gmultiset A). - Provides a bunch of lemmas for
*:on multisets - Extends
multiset_solverand adds a couple of tests.
Edited by Robbert Krebbers