Commit 2023-01-22 11:32 ae5357f9

View on Github →

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.

Estimated changes

Created src/data/finsupp/alist.lean

added theorem alist.empty_lookup_finsupp

added theorem alist.insert_lookup_finsupp

added theorem alist.lookup_finsupp_apply

added theorem alist.lookup_finsupp_eq_iff_of_ne_zero

added theorem alist.lookup_finsupp_eq_zero_iff

added theorem alist.lookup_finsupp_support

added theorem alist.lookup_finsupp_surjective

added theorem alist.singleton_lookup_finsupp

added theorem finsupp.mem_to_alist

added theorem finsupp.to_alist_keys_to_finset

added theorem finsupp.to_alist_lookup_finsupp

Modified src/data/finsupp/basic.lean

deleted theorem alist.empty_lookup_finsupp

deleted theorem alist.insert_lookup_finsupp

deleted def alist.lookup_finsupp

deleted theorem alist.lookup_finsupp_apply

deleted theorem alist.lookup_finsupp_eq_iff_of_ne_zero

deleted theorem alist.lookup_finsupp_eq_zero_iff

deleted theorem alist.lookup_finsupp_support

deleted theorem alist.lookup_finsupp_surjective

deleted theorem alist.singleton_lookup_finsupp

deleted theorem finsupp.mem_to_alist

deleted def finsupp.to_alist

deleted theorem finsupp.to_alist_keys_to_finset

deleted theorem finsupp.to_alist_lookup_finsupp