Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2019-07-13 01:46
6db58292
View on Github →
feat(data/finmap): extend the API (
#1223
)
Estimated changes
Modified
src/data/finmap.lean
added
def
finmap.all
added
def
finmap.any
added
theorem
finmap.disjoint.symm
added
theorem
finmap.disjoint.symm_iff
added
def
finmap.disjoint
added
theorem
finmap.disjoint_empty
added
theorem
finmap.disjoint_union_left
added
theorem
finmap.disjoint_union_right
modified
theorem
finmap.empty_to_finmap
added
theorem
finmap.empty_union
added
theorem
finmap.erase_erase
added
theorem
finmap.erase_union_singleton
added
theorem
finmap.ext_lookup
added
theorem
finmap.insert_insert
added
theorem
finmap.insert_insert_of_ne
added
theorem
finmap.insert_singleton_eq
added
theorem
finmap.insert_union
added
theorem
finmap.lookup_insert_of_ne
added
theorem
finmap.lookup_list_to_finmap
added
theorem
finmap.lookup_singleton_eq
added
theorem
finmap.lookup_union_left_of_not_in
added
theorem
finmap.mem_iff
added
theorem
finmap.mem_list_to_finmap
added
theorem
finmap.mem_of_lookup_eq_some
added
theorem
finmap.mem_singleton
added
theorem
finmap.not_mem_erase_self
added
def
finmap.sdiff
added
theorem
finmap.to_finmap_cons
added
theorem
finmap.to_finmap_nil
added
theorem
finmap.union_assoc
added
theorem
finmap.union_cancel
added
theorem
finmap.union_comm_of_disjoint
added
theorem
finmap.union_empty
added
def
list.to_finmap
Modified
src/data/list/alist.lean
added
def
alist.disjoint
added
theorem
alist.entries_to_alist
added
theorem
alist.erase_erase
added
theorem
alist.insert_insert
added
theorem
alist.insert_insert_of_ne
added
theorem
alist.insert_singleton_eq
added
theorem
alist.insert_union
added
theorem
alist.lookup_to_alist
added
theorem
alist.to_alist_cons
added
theorem
alist.union_assoc
added
theorem
alist.union_comm_of_disjoint
added
theorem
alist.union_erase
added
def
list.to_alist
Modified
src/data/list/basic.lean
added
theorem
list.foldl_eq_foldr'
added
theorem
list.foldl_eq_of_comm'
added
theorem
list.foldr_eq_of_comm'
added
theorem
list.mem_enum_from
added
theorem
list.pw_filter_map
Modified
src/data/list/sigma.lean
added
def
list.erase_dupkeys
added
theorem
list.erase_dupkeys_cons
added
theorem
list.kerase_kerase
added
theorem
list.lookup_erase_dupkeys
added
theorem
list.lookup_ext
added
theorem
list.mem_ext
added
theorem
list.nodupkeys_erase_dupkeys