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 → 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
• Provides an instance ScalarMul nat (gmultiset A).
• Provides a bunch of lemmas for *: on multisets
• Extends multiset_solver and adds a couple of tests.

I don't like the name Scalar. That sounds like it would describe a scalar, not a scalar multiplication. I think Mul or something like that needs to appear in the name.

added 16 commits

• aa225cb8...3af97445 - 12 commits from branch master
• bb1d27f6 - Add `ScalarMul` operational type class.
• 65dec1a0 - Add scalar multiplication for multisets.
• 5ab66faa - Comment.
• c81e49b5 - CHANGELOG.

Compare with previous version

changed the description

LGTM apart from some even more detailed comments.

added 1 commit

• 4b789013 - Comments Ralf.

Compare with previous version

resolved all threads

enabled an automatic merge when the pipeline for 4b789013 succeeds

merged

mentioned in commit 0528f023