Commit 2022-11-24 01:48 364d8714

View on Github →

chore(data/list/big_operators): split (#17702) Split data.list.big_operators into .basic and .lemmas, with the former containing no algebra or set imports. This should make more of the fintype dependency tree portable sooner.

Estimated changes

Modified src/algebra/big_operators/multiset.lean

Modified src/algebra/free_monoid/basic.lean

Modified src/algebra/graded_monoid.lean

Modified src/control/fold.lean

Renamed src/data/list/big_operators.lean to src/data/list/big_operators/basic.lean

deleted theorem commute.list_sum_left

deleted theorem commute.list_sum_right

deleted theorem list.alternating_prod_append

deleted theorem list.alternating_prod_reverse

deleted theorem list.dvd_prod

deleted theorem list.dvd_sum

deleted theorem list.length_le_sum_of_one_le

deleted theorem list.neg_one_mem_of_prod_eq_neg_one

deleted theorem list.pow_card_le_prod

deleted theorem list.prod_eq_one_iff

deleted theorem list.sum_map_mul_left

deleted theorem list.sum_map_mul_right

deleted theorem mul_opposite.op_list_prod

deleted theorem mul_opposite.unop_list_prod

deleted theorem unop_map_list_prod

Created src/data/list/big_operators/lemmas.lean

added theorem commute.list_sum_left

added theorem commute.list_sum_right

added theorem list.alternating_prod_append

added theorem list.alternating_prod_reverse

added theorem list.dvd_prod

added theorem list.dvd_sum

added theorem list.length_le_sum_of_one_le

added theorem list.neg_one_mem_of_prod_eq_neg_one

added theorem list.pow_card_le_prod

added theorem list.prod_eq_one_iff

added theorem list.sum_map_mul_left

added theorem list.sum_map_mul_right

added theorem mul_opposite.op_list_prod

added theorem mul_opposite.unop_list_prod

added theorem unop_map_list_prod

Modified src/data/list/count.lean

Modified src/data/list/join.lean

Modified src/data/list/prime.lean

Modified src/data/list/prod_sigma.lean

Modified src/data/list/zip.lean