Mathlib v3 is deprecated. Go to Mathlib v4

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 for further discussion of the motivation.

Estimated changes