Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-11-19 00:41 f9de1839

View on Github →

feat(data/multiset): working on multisets, fix rcases bug

Estimated changes

added theorem max_min_distrib_left
added theorem max_min_distrib_right
added theorem min_max_distrib_left
added theorem min_max_distrib_right
added theorem list.bag_inter_nil
added theorem list.length_bind
added theorem list.length_join
added theorem list.mem_bag_inter
added theorem list.mem_erase_of_ne
added theorem list.nil_bag_inter
added theorem list.nth_range'
added theorem list.nth_range
modified def list.permutations_aux
added theorem list.sum_const_nat
added theorem list.mem_permutations
modified theorem list.perm_diff_right
added theorem list.perm_nil
added theorem multiset.add_bind
added theorem multiset.add_product
added def multiset.bind
added theorem multiset.coe_bind
modified theorem multiset.coe_eq_coe
modified theorem multiset.coe_foldl
modified theorem multiset.coe_foldr
added theorem multiset.coe_map
added theorem multiset.coe_prod
added theorem multiset.coe_product
added theorem multiset.cons_bind
added theorem multiset.cons_product
added theorem multiset.foldl_add
added theorem multiset.foldl_cons
added theorem multiset.foldl_zero
added theorem multiset.foldr_add
added theorem multiset.foldr_cons
added theorem multiset.foldr_zero
added def multiset.inter
modified theorem multiset.inter_comm
added theorem multiset.inter_le_left
added theorem multiset.inter_zero
added theorem multiset.join_add
added theorem multiset.join_cons
added theorem multiset.join_zero
added theorem multiset.le_inter
modified theorem multiset.le_union_left
modified theorem multiset.le_union_right
added theorem multiset.map_add
added theorem multiset.map_cons
added theorem multiset.map_map
added theorem multiset.map_zero
added theorem multiset.prod_add
added theorem multiset.prod_cons
added theorem multiset.prod_eq_foldl
added theorem multiset.prod_eq_foldr
added theorem multiset.prod_zero
added def multiset.product
added theorem multiset.product_add
deleted def multiset.sum
modified theorem multiset.union_comm
added theorem multiset.zero_bind
added theorem multiset.zero_inter
added theorem multiset.zero_product
deleted theorem quot_mk_image_univ_eq
added theorem quotient.eq
modified inductive pSet.definable