Commit 2020-07-22 10:18 39f8f020

View on Github →

refactor(algebra/big_operators): split file, reduce imports (#3495) I've split up algebra.big_operators. It wasn't completely obvious how to divide it up, but this is an attempt to balance coherence / file size / minimal imports.

Estimated changes

Modified archive/100-theorems-list/42_inverse_triangle_sum.lean

Modified archive/sensitivity.lean

Renamed src/algebra/big_operators.lean to src/algebra/big_operators/basic.lean

deleted theorem directed.finset_le

deleted theorem finset.abs_sum_le_sum_abs

deleted theorem finset.card_le_mul_card_image

deleted theorem finset.card_pi

deleted theorem finset.dvd_sum

deleted theorem finset.exists_le

deleted theorem finset.exists_le_of_sum_le

deleted theorem finset.exists_pos_of_sum_zero_of_exists_nonzero

deleted theorem finset.le_sum_of_subadditive

deleted theorem finset.mul_sum

deleted theorem finset.prod_Ico_add

deleted theorem finset.prod_Ico_consecutive

deleted theorem finset.prod_Ico_eq_mul_inv

deleted theorem finset.prod_Ico_eq_prod_range

deleted theorem finset.prod_Ico_id_eq_fact

deleted theorem finset.prod_Ico_reflect

deleted theorem finset.prod_Ico_succ_top

deleted theorem finset.prod_add

deleted theorem finset.prod_eq_prod_Ico_succ_bot

deleted theorem finset.prod_le_prod'

deleted theorem finset.prod_le_prod

deleted theorem finset.prod_nat_cast

deleted theorem finset.prod_nonneg

deleted theorem finset.prod_pos

deleted theorem finset.prod_pow_eq_pow_sum

deleted theorem finset.prod_powerset_insert

deleted theorem finset.prod_range_mul_prod_Ico

deleted theorem finset.prod_range_reflect

deleted theorem finset.prod_sum

deleted theorem finset.single_le_sum

deleted theorem finset.sum_Ico_add

deleted theorem finset.sum_Ico_eq_sub

deleted theorem finset.sum_Ico_reflect

deleted theorem finset.sum_Ico_succ_top

deleted theorem finset.sum_boole_mul

deleted theorem finset.sum_div

deleted theorem finset.sum_eq_sum_Ico_succ_bot

deleted theorem finset.sum_eq_zero_iff

deleted theorem finset.sum_eq_zero_iff_of_nonneg

deleted theorem finset.sum_eq_zero_iff_of_nonpos

deleted theorem finset.sum_le_sum

deleted theorem finset.sum_le_sum_of_ne_zero

deleted theorem finset.sum_le_sum_of_subset

deleted theorem finset.sum_le_sum_of_subset_of_nonneg

deleted theorem finset.sum_lt_sum

deleted theorem finset.sum_lt_sum_of_nonempty

deleted theorem finset.sum_lt_sum_of_subset

deleted theorem finset.sum_mono_set

deleted theorem finset.sum_mono_set_of_nonneg

deleted theorem finset.sum_mul

deleted theorem finset.sum_mul_boole

deleted theorem finset.sum_mul_sum

deleted theorem finset.sum_nonneg

deleted theorem finset.sum_nonpos

deleted theorem finset.sum_pow_mul_eq_add_pow

deleted theorem finset.sum_range_id

deleted theorem finset.sum_range_id_mul_two

deleted theorem finset.sum_range_reflect

deleted theorem is_group_hom_finset_prod

deleted theorem with_top.op_sum

deleted theorem with_top.sum_eq_top_iff

deleted theorem with_top.sum_lt_top

deleted theorem with_top.sum_lt_top_iff

deleted theorem with_top.unop_sum

Created src/algebra/big_operators/default.lean

Created src/algebra/big_operators/intervals.lean

added theorem finset.prod_Ico_add

added theorem finset.prod_Ico_consecutive

added theorem finset.prod_Ico_eq_mul_inv

added theorem finset.prod_Ico_eq_prod_range

added theorem finset.prod_Ico_id_eq_fact

added theorem finset.prod_Ico_reflect

added theorem finset.prod_Ico_succ_top

added theorem finset.prod_eq_prod_Ico_succ_bot

added theorem finset.prod_range_mul_prod_Ico

added theorem finset.prod_range_reflect

added theorem finset.sum_Ico_add

added theorem finset.sum_Ico_eq_sub

added theorem finset.sum_Ico_reflect

added theorem finset.sum_Ico_succ_top

added theorem finset.sum_eq_sum_Ico_succ_bot

added theorem finset.sum_range_id

added theorem finset.sum_range_id_mul_two

added theorem finset.sum_range_reflect

Created src/algebra/big_operators/order.lean

added theorem finset.abs_sum_le_sum_abs

added theorem finset.card_le_mul_card_image

added theorem finset.exists_le_of_sum_le

added theorem finset.exists_pos_of_sum_zero_of_exists_nonzero

added theorem finset.le_sum_of_subadditive

added theorem finset.prod_le_prod'

added theorem finset.prod_le_prod

added theorem finset.prod_nonneg

added theorem finset.prod_pos

added theorem finset.single_le_sum

added theorem finset.sum_eq_zero_iff

added theorem finset.sum_eq_zero_iff_of_nonneg

added theorem finset.sum_eq_zero_iff_of_nonpos

added theorem finset.sum_le_sum

added theorem finset.sum_le_sum_of_ne_zero

added theorem finset.sum_le_sum_of_subset

added theorem finset.sum_le_sum_of_subset_of_nonneg

added theorem finset.sum_lt_sum

added theorem finset.sum_lt_sum_of_nonempty

added theorem finset.sum_lt_sum_of_subset

added theorem finset.sum_mono_set

added theorem finset.sum_mono_set_of_nonneg

added theorem finset.sum_nonneg

added theorem finset.sum_nonpos

added theorem with_top.op_sum

added theorem with_top.sum_eq_top_iff

added theorem with_top.sum_lt_top

added theorem with_top.sum_lt_top_iff

added theorem with_top.unop_sum

Created src/algebra/big_operators/ring.lean

added theorem finset.dvd_sum

added theorem finset.mul_sum

added theorem finset.prod_add

added theorem finset.prod_nat_cast

added theorem finset.prod_pow_eq_pow_sum

added theorem finset.prod_powerset_insert

added theorem finset.prod_sum

added theorem finset.sum_boole_mul

added theorem finset.sum_div

added theorem finset.sum_mul

added theorem finset.sum_mul_boole

added theorem finset.sum_mul_sum

added theorem finset.sum_pow_mul_eq_add_pow

Modified src/algebra/direct_limit.lean

Modified src/algebra/geom_sum.lean

Modified src/algebra/module.lean

deleted theorem finset.exists_card_smul_ge_sum

deleted theorem finset.exists_card_smul_le_sum

deleted theorem finset.sum_const'

Modified src/category_theory/limits/shapes/biproducts.lean

Modified src/category_theory/preadditive/default.lean

Created src/data/finset/order.lean

added theorem directed.finset_le

added theorem finset.exists_le

Modified src/data/finsupp.lean

Modified src/data/fintype/card.lean

added theorem finset.card_pi

Modified src/data/matrix/basic.lean

Modified src/data/nat/choose.lean

Modified src/data/nat/multiplicity.lean

Modified src/data/nat/totient.lean

Modified src/data/real/cau_seq.lean

Modified src/data/real/nnreal.lean

Modified src/data/set/finite.lean

Modified src/data/support.lean

Modified src/group_theory/order_of_element.lean

Modified src/group_theory/perm/sign.lean

Modified src/group_theory/submonoid/membership.lean

Modified src/linear_algebra/basis.lean

Modified src/linear_algebra/lagrange.lean

Modified src/linear_algebra/multilinear.lean

Modified src/ring_theory/coprime.lean

Modified src/ring_theory/multiplicity.lean

Modified src/ring_theory/prime.lean

Modified src/topology/algebra/infinite_sum.lean

Modified src/topology/metric_space/emetric_space.lean

Modified src/topology/subset_properties.lean

Modified test/conv/apply_congr.lean

Modified test/fin_cases.lean