Commit 2023-01-16 14:40 5f2a4636

View on Github →

style: Nodupkeys -> no/NodupKeys dedupkeys -> dedupKeys (#1592) As per the comments here.

Estimated changes

Modified Mathlib/Data/List/AList.lean

modified theorem AList.entries_to_alist

modified def List.toAList

Modified Mathlib/Data/List/Sigma.lean

added theorem List.NodupKeys.eq_of_fst_eq

added theorem List.NodupKeys.eq_of_mk_mem

added theorem List.NodupKeys.kerase

added theorem List.NodupKeys.kunion

added theorem List.NodupKeys.pairwise_ne

added theorem List.NodupKeys.sublist

added def List.NodupKeys

deleted theorem List.Nodupkeys.eq_of_fst_eq

deleted theorem List.Nodupkeys.eq_of_mk_mem

deleted theorem List.Nodupkeys.kerase

deleted theorem List.Nodupkeys.kunion

deleted theorem List.Nodupkeys.pairwise_ne

deleted theorem List.Nodupkeys.sublist

deleted def List.Nodupkeys

modified theorem List.Perm.kerase

modified theorem List.Perm.kinsert

modified theorem List.Perm.kreplace

modified theorem List.Perm.kunion

added def List.dedupKeys

added theorem List.dedupKeys_cons

deleted def List.dedupkeys

deleted theorem List.dedupkeys_cons

added theorem List.dlookup_dedupKeys

deleted theorem List.dlookup_dedupkeys

modified theorem List.dlookup_kerase

added theorem List.kinsert_nodupKeys

deleted theorem List.kinsert_nodupkeys

added theorem List.kreplace_nodupKeys

deleted theorem List.kreplace_nodupkeys

modified theorem List.kreplace_self

modified theorem List.lookupAll_eq_dlookup

modified theorem List.lookupAll_length_le_one

modified theorem List.lookupAll_nodup

modified theorem List.lookup_ext

modified theorem List.mem_dlookup

modified theorem List.mem_dlookup_iff

added theorem List.nodupKeys_cons

added theorem List.nodupKeys_dedupKeys

added theorem List.nodupKeys_iff_pairwise

added theorem List.nodupKeys_join

added theorem List.nodupKeys_nil

added theorem List.nodupKeys_singleton

deleted theorem List.nodupkeys_cons

deleted theorem List.nodupkeys_dedupkeys

deleted theorem List.nodupkeys_iff_pairwise

deleted theorem List.nodupkeys_join

deleted theorem List.nodupkeys_nil

deleted theorem List.nodupkeys_singleton

modified theorem List.not_mem_keys_kerase

modified theorem List.perm_dlookup

modified theorem List.perm_lookupAll

added theorem List.perm_nodupKeys

deleted theorem List.perm_nodupkeys

added theorem List.sizeOf_dedupKeys

deleted theorem List.sizeOf_dedupkeys