mathlib

036348ae - chore(data/multiset/nodup): remove dependency on `multiset.powerset` (#17888)

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`.