mathlib3
6b2bb8a1 - feat(data/finsupp): to_multiset symm apply (#7356)

Commit

4 years ago

feat(data/finsupp): to_multiset symm apply (#7356) Adds a lemma and golfs a proof.

Author

b-mehta

Parents