Reorganising DFinsupp

Stream: mathlib4

[Yaël Dillies]

I want to record on Zulip a message I wrote on #12493 regarding the optimal file layout I envision for DFinsupp/Finsupp. Here it is:
Yaël Dillies said:

The fact that you are removing the IsCentralScalar instance but not the IsScalarTower one makes me think you're doing something wrong. Reading through, I am not getting a feeling I understand what should be in this file vs Data.DFinsupp.Lemmas.

Here is a suggestion: People (eg @__Sky Wilshaw) have wanted finitely supported functions where the support is not the set of elements not sent to 0, but instead the set of elements not sent to a specific fixed element a. Tentatively, this means that Finsupp/DFinsupp have an interpretation as non-algebraic objects and that we should:

• Have a file/folder under Data for everything that can be said about Finsupp/DFinsupp without algebra (past the use of 0, for now)
• Have a file/folder under Algebra for algebraic uses (most of the material we currently have, I think)
• Have a file/folder under Order for purely order theoretic uses (there is currently very little of that)
• Have a file/folder under Algebra.Order for the algebraic order theoretic uses (that we have a bit)

Also note that when thou change DFinsupp, thou shalt change Finsupp too. I'm happy for it to be in a separate PR to avoid having to shuffle everything twice until I give you the green light, though.