Commit 2025-02-25 17:02 614c9c9c

chore(Data/Multiset): split Multiset/Basic.lean into many files (#22126) This PR splits the very large file Mathlib.Data.Multiset.Basic into many files. In particular, my goal was to reduce the dependencies for Mathlib.Data.Finset.Defs. The files created in this split are:

• Multiset.Defs: definition of Multiset, predicates such as membership, order, subsets, remaining definitions required for Finset.Defs. (Some material from Multiset.Nodup was moved here.)
• Multiset.ZeroCons: definition of the empty, singleton and cons operations, induction principles.
• Multiset.Count: definition of count, extensionality principles.
• Multiset.AddSub: definition of addition, erase and subtraction operations.
• Multiset.Replicate: definition of replicate operation.
• Multiset.MapFold: definition of map, foldl and foldr operations.
• Multiset.Filter: definition of filter, filterMap operations.
• Multiset.UnionInter: definition of union, intersection operations and distributive lattice instance.
• Multiset.Basic: miscellaneous results. Nearly each file in this list imports the one above it. I don't know if we can improve the linearity in this bit of the import graph much, but at least the transitive imports should improve a bit I expect. The files with notable modifications are:
• Multiset.Nodup: definition and basic properties of Multiset.Nodup is upstreamed to Multiset.Defs (for use in Finset.Defs).
• Finset.Defs: downstreamed a few declarations to reduce dependencies to only Multiset.Defs. I want to try two extra cleanups, which I'll leave to follow-up PRs in order to make the diff not too ridiculous:
• Upstream more material from Multiset.Nodup
• Reverse the direction of the Multiset.Filter -> Multiset.MapFold import (since there are quite a few results on map that are proved using filter).