Commit 2024-11-11 13:54 19ffdd50

chore(Data/DFinsupp): split Basic.lean into many smaller files (#18656) This PR splits Data/DFinsupp/Basic.lean into a collection of smaller files. The goal here is to keep the structure somewhat intact. Thankfully a somewhat clean split was possible while keeping imports reasonably small. The following new files were made:

• Data/DFinsupp/Defs.lean has the definition of DFinsupp and all the essential definitions: support, single, update, the AddCommMonoid structure. (Or should this be renamed to Basic.lean?)
• Data/DFinsupp/Ext.lean has an extensionality principle for AddMonoidHoms composed with DFinsupps. Might go into Defs.lean except it needs some heavy imports.
• Data/DFinsupp/BigOperators.lean: sums and products of DFinsupps, and sums and products as DFinsupps
• Data/DFinsupp/FiniteInfinite.lean: instances for Fintype and Infinite
• Data/DFinsupp/Module.lean: scalar multiplication and module structure; the DFinsupp maps as linear maps
• Data/DFinsupp/Sigma.lean: sigmaCurry and sigmaUncurry
• Data/DFinsupp/Submonoid.lean: lemmas involving submonoids, in particular that (additive) submonoids are closed under products (sums) of DFinsupps The following file no longer exists:
• Data/DFinsupp/Basic.lean (split completely!)