Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-08 10:06 32c8445a

View on Github →

split(data/list/*): split off data.list.basic (#10164) Killing the giants. This moves 700 lines off data.list.basic that were about

  • list.sum and list.product into data.list.big_operators
  • list.countp and list.count into data.list.count
  • list.sigma and list.prod into data.list.sigma_prod

Estimated changes

deleted theorem list.alternating_prod_nil
deleted theorem list.count_append
deleted theorem list.count_bind
deleted theorem list.count_concat
deleted theorem list.count_cons'
deleted theorem list.count_cons
deleted theorem list.count_cons_of_ne
deleted theorem list.count_cons_self
deleted theorem list.count_erase_of_ne
deleted theorem list.count_erase_self
deleted theorem list.count_filter
deleted theorem list.count_le_count_cons
deleted theorem list.count_le_of_sublist
deleted theorem list.count_map_map
deleted theorem list.count_nil
deleted theorem list.count_pos
deleted theorem list.count_repeat
deleted theorem list.count_singleton
deleted theorem list.count_tail
deleted theorem list.countp_append
deleted theorem list.countp_cons_of_neg
deleted theorem list.countp_cons_of_pos
deleted theorem list.countp_filter
deleted theorem list.countp_le_of_sublist
deleted theorem list.countp_nil
deleted theorem list.countp_pos
deleted theorem list.drop_sum_join
deleted theorem list.dvd_prod
deleted theorem list.dvd_sum
deleted theorem list.eq_iff_join_eq
deleted theorem list.eq_of_sum_take_eq
deleted theorem list.exists_le_of_sum_le
deleted theorem list.exists_lt_of_sum_lt
deleted theorem list.head_add_tail_sum
deleted theorem list.head_le_sum
deleted theorem list.join_append
deleted theorem list.join_eq_nil
deleted theorem list.join_filter_ne_nil
deleted theorem list.join_join
deleted theorem list.join_nil
deleted theorem list.length_bind
deleted theorem list.length_join
deleted theorem list.length_product
deleted theorem list.length_sigma
modified theorem list.mem_map_swap
deleted theorem list.mem_product
deleted theorem list.mem_sigma
deleted theorem list.monotone_sum_take
deleted theorem list.nil_product
deleted theorem list.nil_sigma
deleted theorem list.nth_le_join
deleted theorem list.prod_append
deleted theorem list.prod_concat
deleted theorem list.prod_cons
deleted theorem list.prod_drop_succ
deleted theorem list.prod_eq_foldr
deleted theorem list.prod_eq_zero
deleted theorem list.prod_eq_zero_iff
deleted theorem list.prod_erase
deleted theorem list.prod_hom
deleted theorem list.prod_hom_rel
deleted theorem list.prod_inv
deleted theorem list.prod_inv_reverse
deleted theorem list.prod_is_unit
deleted theorem list.prod_join
deleted theorem list.prod_map_hom
deleted theorem list.prod_ne_zero
deleted theorem list.prod_nil
deleted theorem list.prod_pos
deleted theorem list.prod_reverse_noncomm
deleted theorem list.prod_singleton
deleted theorem list.prod_take_succ
deleted theorem list.prod_update_nth'
deleted theorem list.prod_update_nth
deleted theorem list.product_cons
deleted theorem list.product_nil
deleted theorem list.sigma_cons
deleted theorem list.sigma_nil
deleted theorem list.single_le_prod
modified theorem list.sizeof_slice_lt
modified theorem list.slice_eq
deleted theorem list.sum_const_nat
deleted theorem list.sum_eq_zero_iff
deleted theorem list.sum_le_foldr_max
deleted theorem list.sum_map_mul_left
deleted theorem list.sum_map_mul_right
deleted theorem list.tail_sum
deleted theorem list.take_sum_join
deleted theorem monoid_hom.map_list_prod
deleted theorem opposite.op_list_prod
deleted theorem opposite.unop_list_prod
added theorem list.dvd_prod
added theorem list.dvd_sum
added theorem list.eq_of_sum_take_eq
added theorem list.head_add_tail_sum
added theorem list.head_le_sum
added theorem list.monotone_sum_take
added theorem list.prod_append
added theorem list.prod_concat
added theorem list.prod_cons
added theorem list.prod_drop_succ
added theorem list.prod_eq_foldr
added theorem list.prod_eq_zero
added theorem list.prod_eq_zero_iff
added theorem list.prod_erase
added theorem list.prod_hom
added theorem list.prod_hom_rel
added theorem list.prod_inv
added theorem list.prod_inv_reverse
added theorem list.prod_is_unit
added theorem list.prod_join
added theorem list.prod_map_hom
added theorem list.prod_ne_zero
added theorem list.prod_nil
added theorem list.prod_pos
added theorem list.prod_singleton
added theorem list.prod_take_succ
added theorem list.prod_update_nth'
added theorem list.prod_update_nth
added theorem list.single_le_prod
added theorem list.sum_const_nat
added theorem list.sum_eq_zero_iff
added theorem list.sum_le_foldr_max
added theorem list.sum_map_mul_left
added theorem list.sum_map_mul_right
added theorem list.tail_sum
added theorem opposite.op_list_prod
added theorem list.count_append
added theorem list.count_bind
added theorem list.count_concat
added theorem list.count_cons'
added theorem list.count_cons
added theorem list.count_cons_of_ne
added theorem list.count_cons_self
added theorem list.count_erase_of_ne
added theorem list.count_erase_self
added theorem list.count_filter
added theorem list.count_map_map
added theorem list.count_nil
added theorem list.count_pos
added theorem list.count_repeat
added theorem list.count_singleton
added theorem list.count_tail
added theorem list.countp_append
added theorem list.countp_filter
added theorem list.countp_nil
added theorem list.countp_pos
added theorem list.sublist.count_le
added theorem list.sublist.countp_le
added theorem list.drop_sum_join
added theorem list.eq_iff_join_eq
added theorem list.join_append
added theorem list.join_eq_nil
added theorem list.join_join
added theorem list.join_nil
added theorem list.length_bind
added theorem list.length_join
added theorem list.nth_le_join
added theorem list.take_sum_join
added theorem list.length_product
added theorem list.length_sigma
added theorem list.mem_product
added theorem list.mem_sigma
added theorem list.nil_product
added theorem list.nil_sigma
added theorem list.product_cons
added theorem list.product_nil
added theorem list.sigma_cons
added theorem list.sigma_nil