Add `gmultiset_map` and associated lemmas

This merge request adds a definition for mapping over a gmultiset, gmultiset_map, similar to set_map for (regular) finite sets.

I struggled with finding a correct location for the definition and associated lemmas in gmultiset.v. I am open to any suggestions to improve the placement.

added 1 commit

• a1d0c311 - Remove superfluous type hints

Compare with previous version

added 1 commit

• 70772e14 - Explicitly name IH

Compare with previous version

added 1 commit

• 88a3baa1 - Actually give an explicit name to the IH

Compare with previous version

changed the description

added 1 commit

• 65f28290 - Add lemma about injectivity of gmultiset_map when 'f' is injective

Compare with previous version

added 1 commit

• 3f7421c7 - Use unicode arrow

Compare with previous version

added 3 commits

• 2cbe4b4f - Slightly simplify proof
• e7405db5 - Improve styling
• f2098383 - Rewrite injectivity lemma to instance of Inj

Compare with previous version

added 1 commit

• 63835cb3 - Move definition to top

Compare with previous version

added 2 commits

• bfc40224 - Version of `gmultiset_map` that avoids converting to lists.
• 862e4bc5 - CHANGELOG.

Compare with previous version

Thanks for the MR and implementing the suggested changes.

I tweaked gmultiset_map a bit so as to avoid converting to lists and back. I proved a lemma gmultiset_map_alt with the original (and more easy to use) definition.

@jung As far as I am concerned this one is ready.

enabled an automatic merge when all merge checks for 862e4bc5 pass

resolved all threads

mentioned in commit 4d307c87