mathlib

ae5357f9 - refactor(data/finsupp/basic): split out alist results (#18250)

refactor(data/finsupp/basic): split out alist results (#18250) 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.