Mathlib v3 is deprecated. Go to Mathlib v4

Theorem list.not_mem_keys_of_nodupkeys_cons

Modification history

2023-01-20 00:18

src/data/list/sigma.lean

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

Added list.not_mem_keys_of_nodupkeys_cons View on Github →