Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-25 19:14 8d426f04

View on Github →

split(algebra/big_operators/multiset): Split off data.multiset.basic (#11043) This moves

  • multiset.prod, multiset.sum to algebra.big_operators.multiset
  • multiset.join, multiset.bind, multiset.product, multiset.sigma to data.multiset.bind. This is needed as join is defined using sum. The file was quite messy, so I reorganized algebra.big_operators.multiset by increasing typeclass assumptions. I'm crediting Mario for 0663945f55335e51c2b9b3a0177a84262dd87eaf (prod, sum, join), f9de18397dc1a43817803c2fe5d84b282287ed0d (bind, product), 16d40d7491d1fe8a733d21e90e516e0dd3f41c5b (sigma).

Estimated changes

added theorem multiset.coe_prod
added theorem multiset.dvd_prod
added theorem multiset.dvd_sum
added theorem multiset.le_sum_of_mem
added theorem multiset.pow_count
added def multiset.prod
added theorem multiset.prod_add
added theorem multiset.prod_cons
added theorem multiset.prod_dvd_prod
added theorem multiset.prod_eq_foldl
added theorem multiset.prod_eq_foldr
added theorem multiset.prod_eq_zero
added theorem multiset.prod_hom
added theorem multiset.prod_hom_rel
added theorem multiset.prod_map_inv
added theorem multiset.prod_map_mul
added theorem multiset.prod_map_one
added theorem multiset.prod_ne_zero
added theorem multiset.prod_nonneg
added theorem multiset.prod_nsmul
added theorem multiset.prod_repeat
added theorem multiset.prod_to_list
added theorem multiset.prod_zero
deleted theorem multiset.add_bind
deleted theorem multiset.add_product
deleted theorem multiset.add_sigma
deleted def multiset.bind
deleted theorem multiset.bind_add
deleted theorem multiset.bind_assoc
deleted theorem multiset.bind_bind
deleted theorem multiset.bind_congr
deleted theorem multiset.bind_cons
deleted theorem multiset.bind_hcongr
deleted theorem multiset.bind_map
deleted theorem multiset.bind_map_comm
deleted theorem multiset.bind_singleton
deleted theorem multiset.bind_zero
deleted theorem multiset.card_bind
deleted theorem multiset.card_join
deleted theorem multiset.card_product
deleted theorem multiset.card_sigma
deleted theorem multiset.coe_bind
deleted theorem multiset.coe_join
deleted theorem multiset.coe_prod
deleted theorem multiset.coe_product
deleted theorem multiset.coe_sigma
deleted theorem multiset.cons_bind
deleted theorem multiset.cons_product
deleted theorem multiset.cons_sigma
deleted theorem multiset.count_bind
deleted theorem multiset.count_sum
deleted theorem multiset.dvd_prod
deleted theorem multiset.dvd_sum
deleted def multiset.join
deleted theorem multiset.join_add
deleted theorem multiset.join_cons
deleted theorem multiset.join_zero
deleted theorem multiset.le_sum_of_mem
deleted theorem multiset.map_bind
deleted theorem multiset.mem_bind
deleted theorem multiset.mem_join
deleted theorem multiset.mem_product
deleted theorem multiset.mem_sigma
deleted theorem multiset.pow_count
deleted def multiset.prod
deleted theorem multiset.prod_add
deleted theorem multiset.prod_bind
deleted theorem multiset.prod_cons
deleted theorem multiset.prod_dvd_prod
deleted theorem multiset.prod_eq_foldl
deleted theorem multiset.prod_eq_foldr
deleted theorem multiset.prod_eq_zero
deleted theorem multiset.prod_eq_zero_iff
deleted theorem multiset.prod_hom
deleted theorem multiset.prod_hom_rel
deleted theorem multiset.prod_induction
deleted theorem multiset.prod_map_inv
deleted theorem multiset.prod_map_mul
deleted theorem multiset.prod_map_one
deleted theorem multiset.prod_ne_zero
deleted theorem multiset.prod_nonneg
deleted theorem multiset.prod_nsmul
deleted theorem multiset.prod_repeat
deleted theorem multiset.prod_singleton
deleted theorem multiset.prod_to_list
deleted theorem multiset.prod_zero
deleted def multiset.product
deleted theorem multiset.product_add
deleted theorem multiset.rel_bind
deleted theorem multiset.rel_join
deleted theorem multiset.sigma_add
deleted theorem multiset.sigma_singleton
deleted theorem multiset.single_le_prod
deleted theorem multiset.singleton_bind
deleted theorem multiset.singleton_join
deleted theorem multiset.sum_eq_zero_iff
deleted theorem multiset.sum_le_sum_map
deleted theorem multiset.sum_map_le_sum
deleted theorem multiset.sum_map_mul_left
deleted theorem multiset.zero_bind
deleted theorem multiset.zero_product
deleted theorem multiset.zero_sigma
added theorem multiset.add_bind
added theorem multiset.add_product
added theorem multiset.add_sigma
added def multiset.bind
added theorem multiset.bind_add
added theorem multiset.bind_assoc
added theorem multiset.bind_bind
added theorem multiset.bind_congr
added theorem multiset.bind_cons
added theorem multiset.bind_hcongr
added theorem multiset.bind_map
added theorem multiset.bind_map_comm
added theorem multiset.bind_zero
added theorem multiset.card_bind
added theorem multiset.card_join
added theorem multiset.card_product
added theorem multiset.card_sigma
added theorem multiset.coe_bind
added theorem multiset.coe_join
added theorem multiset.coe_product
added theorem multiset.coe_sigma
added theorem multiset.cons_bind
added theorem multiset.cons_product
added theorem multiset.cons_sigma
added theorem multiset.count_bind
added theorem multiset.count_sum
added def multiset.join
added theorem multiset.join_add
added theorem multiset.join_cons
added theorem multiset.join_zero
added theorem multiset.map_bind
added theorem multiset.mem_bind
added theorem multiset.mem_join
added theorem multiset.mem_product
added theorem multiset.mem_sigma
added theorem multiset.prod_bind
added def multiset.product
added theorem multiset.product_add
added theorem multiset.rel_bind
added theorem multiset.rel_join
added theorem multiset.sigma_add
added theorem multiset.zero_bind
added theorem multiset.zero_product
added theorem multiset.zero_sigma