Commit 2024-02-28 00:59 ae9f685e

chore(Algebra/BigOperators): reduce imports for Multiset.prod (#10987) I noticed that BigOperators/Multiset/Basic.lean transitively imports a lot of files, and it sits on the longest pole. If we move one lemma to another file, we can severely restrict the amount of imports required. Looks like the extra imports that shake didn't notice were due to instances being filled in that we didn't actually need.