Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-20 00:18 f808feb6

View on Github →

feat(data/list/alist): recursion on alist using insert (#15434)

Estimated changes

Modified src/data/list/alist.lean

added theorem alist.insert_of_neg

added def alist.insert_rec

added theorem alist.insert_rec_empty

added theorem alist.insert_rec_insert

added theorem alist.mk_cons_eq_insert

added theorem alist.recursion_insert_mk

Modified src/data/list/sigma.lean

added theorem list.nodupkeys_of_nodupkeys_cons

added theorem list.not_mem_keys_of_nodupkeys_cons