[Merged by Bors] - refactor(data/finsupp/basic): split out alist results

[eric-wieser]

This file is getting quite long, and nothing else builds upon these results.

These lemmas and definitions are copied without modification. They were originally from #15443.

---

• depends on: [Merged by Bors] - fix(data/finsupp/basic): add missing decidable arguments in lemma statements #18241

The first commit is from that PR.

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - fix(data/finsupp/basic): add missing decidable arguments in lemma statements #18241
  By Dependent Issues (🤖). Happy coding!

[vihdzp]

These results will be built upon once I develop the set_theory/ordinal/cantor_normal_form.lean file further. The idea (as explained in #16010) is to first define the Cantor Normal Form of an ordinal as an association list, and then use these functions to easily talk about the coefficients.

That rant aside, this LGTM.

[eric-wieser]

Oh absolutely, I'm not saying that the results will never be used; just that they're not likely to be used by anything else in finsupp/basic, and since the file is already large, should probably be in a new file.

[YaelDillies]

I agree this is a useful split. I checked and the only difference introduced is that you haven't opened the finset and function namespaces.

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[sgouezel]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests