Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-11-06 01:26 0947f962

View on Github →

feat(data/multiset): working on multiset.union

Estimated changes

Modified algebra/group.lean

Modified data/int/basic.lean

added theorem int.mul_sign

Modified data/list/basic.lean

added theorem list.erase_sublist_erase

added theorem list.sublist_or_mem_of_sublist

Modified data/multiset/basic.lean

modified theorem multiset.add_cons

added theorem multiset.add_sub_cancel

added theorem multiset.add_sub_cancel_left

modified theorem multiset.add_sub_of_le

added theorem multiset.cons_add

modified theorem multiset.eq_cons_erase

added theorem multiset.eq_union_left

added theorem multiset.eq_union_right

added theorem multiset.erase_le_erase

added theorem multiset.erase_le_iff_le_cons

added theorem multiset.insert_eq_cons

added theorem multiset.le_cons_erase

added theorem multiset.le_cons_of_not_mem

added theorem multiset.le_sub_add

added theorem multiset.le_union_left

added theorem multiset.le_union_right

modified theorem multiset.mem_singleton

modified theorem multiset.mem_singleton_self

added def multiset.ndinsert

added def multiset.nodup

modified theorem multiset.singleton_inj

modified theorem multiset.singleton_ne_zero

modified theorem multiset.sub_add_cancel

added theorem multiset.sub_le_iff_le_add

added theorem multiset.sub_le_sub_left

added theorem multiset.sub_le_sub_right

added def multiset.union

added theorem multiset.union_comm

added theorem multiset.union_le

added theorem multiset.union_le_union_left

added theorem multiset.union_le_union_right