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.
Edited by Robbert Krebbers