[Merged by Bors] - chore(data/multiset/nodup): remove dependency on multiset.powerset

[FR-vdash-bot]

This flips the import direction between data.multiset.powerset and data.multiset.nodup, such that the former now imports the latter, moving lemmas as necessary.

This matches how data.list.sublists (transitively) imports data.list.nodup.

More importantly, this means that finset (which needs multiset.nodup) can be defined without needing the material on list.sublists and multiset.powerset.

---

[eric-wieser]

What's the motivation for this move? It's not clear to me that either of nodup or powerset is the more primitive operation, which favors doing nothing to avoid churn.

Of course, if you wrote a PR description explaining your motivation you might be able to persuade me otherwise :)

[FR-vdash-bot]

data.multiset.powerset imports more things (data.list.sublists) than data.multiset.nodup. data.multiset.nodup is not avoidable for finset, we want to make it import less things.

[eric-wieser]

Ah thanks; finset needs nodup but not powerset.

I think this change makes sense; can you fix the build failure?

[eric-wieser]

I've copy-edited your PR description to emphasize the important bits.

Can you add a assert_not_exists list.sublists to finset/basic.lean, assuming it doesn't error?

[eric-wieser]

bors d+

Thanks!

[bors]

✌️ negiizhao can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[FR-vdash-bot]

list.sublists is in data.list.defs. I added assert_not_exists list.sublists_len.

[eric-wieser]

Can you add a comment to that effect above the assert_not_exists?

[FR-vdash-bot]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

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