Commit 2023-02-02 05:25 fb2c4228

View on Github →

feat Port/Data.Finsupp.AList (#1991) port of data.finsupp.alist

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Finsupp/AList.lean

added theorem AList.empty_lookupFinsupp

added theorem AList.insert_lookupFinsupp

added theorem AList.lookupFinsupp_apply

added theorem AList.lookupFinsupp_eq_iff_of_ne_zero

added theorem AList.lookupFinsupp_eq_zero_iff

added theorem AList.lookupFinsupp_support

added theorem AList.lookupFinsupp_surjective

added theorem AList.singleton_lookupFinsupp

added theorem Finsupp.mem_toAlist

added theorem Finsupp.toAList_keys_toFinset

added theorem Finsupp.toAList_lookupFinsupp