Commit 2022-12-10 19:33 036348ae

chore(data/multiset/nodup): remove dependency on multiset.powerset (#17888) 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.