The operation n *: X
multiplies the multiplicity of each element x ∈ X
with n
This MR:
ScalarMul N A := N → A → A
with 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
ScalarMul nat (gmultiset A)
.*:
on multisetsmultiset_solver
and adds a couple of tests.