[Merged by Bors] - feat (data/multiset/powerset): add bind_powerset_len

[xroblot]

We prove the following result

lemma multiset.bind_powerset_len {α : Type*} (S : multiset α) :
  bind (multiset.range (S.card + 1)) (λ k, S.powerset_len k) = S.powerset

From flt-regular

---

• depends on: [Merged by Bors] - feat(data/list/perm): binding all the sublists of a given length gives all the sublists #15834

[eric-wieser]

I wonder if we can derive any of these results from #15834...

[xroblot]

It does look like the sum version could be derived from range_bind_sublists_len in some way. I have to go now but I can try to make it work tomorrow.

[xroblot]

Ok. So I was able to prove an equivalent version of the sum lemma using the results of #15834. I still have to do the sup version, that should be easy but I have to go to bed now. The results have moved to data/multiset/powerset due to the different dependencies.

[xroblot]

Everything is in place now with the new version of sup_powerset_len

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(data/list/perm): binding all the sublists of a given length gives all the sublists #15834
  By Dependent Issues (🤖). Happy coding!

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests