Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-19 13:53 efd9dd3c

View on Github →

feat(data/finsupp/basic): more lemmas on alist.lookup_finsupp (#15875)

Estimated changes

Modified src/data/finsupp/basic.lean

added theorem alist.empty_lookup_finsupp

added theorem alist.insert_lookup_finsupp

added theorem alist.lookup_finsupp_eq_iff_of_ne_zero

added theorem alist.lookup_finsupp_eq_zero_iff

added theorem alist.singleton_lookup_finsupp

deleted theorem alist.to_alist_lookup_finsupp

added theorem finsupp.to_alist_lookup_finsupp

added theorem finsupp.zero_update

Modified src/data/list/alist.lean

added theorem alist.insert_empty

modified theorem alist.not_mem_empty