Commit 2022-08-03 11:38 637b58e8
View on Github →feat(data/finsupp/basic): alist.lookup as a finitely supported function (#15443)
Reworked from #15396. The planned use case for this new definition is to facilitate giving the Cantor Normal Form of an ordinal as a finitely supported function. See https://github.com/leanprover-community/mathlib/pull/15396#discussion_r922723604 for further discussion of the motivation.