Commit 2023-01-18 12:21 2f8a3aa9

View on Github →

feat: port Algebra.BigOperators.Basic (#1628)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/BigOperators/Basic.lean

added theorem Commute.sum_left

added theorem Commute.sum_right

added theorem Equiv.Perm.prod_comp'

added theorem Equiv.Perm.prod_comp

added theorem Finset.Equiv.prod_comp_finset

added theorem Finset.card_bunionᵢ

added theorem Finset.card_bunionᵢ_le

added theorem Finset.card_disjUnionᵢ

added theorem Finset.card_eq_sum_card_fiberwise

added theorem Finset.card_eq_sum_card_image

added theorem Finset.card_eq_sum_ones

added theorem Finset.card_sigma

added theorem Finset.dvd_prod_of_mem

added theorem Finset.eq_of_card_le_one_of_prod_eq

added theorem Finset.eq_one_of_prod_eq_one

added theorem Finset.eq_prod_range_div'

added theorem Finset.eq_prod_range_div

added theorem Finset.eventually_constant_prod

added theorem Finset.exists_ne_one_of_prod_ne_one

added theorem Finset.mem_sum

added theorem Finset.mul_prod_erase

added theorem Finset.nonempty_of_prod_ne_one

added theorem Finset.op_sum

added theorem Finset.pow_eq_prod_const

added theorem Finset.prod_add_prod_eq

added theorem Finset.prod_apply_dite

added theorem Finset.prod_apply_ite

added theorem Finset.prod_apply_ite_of_false

added theorem Finset.prod_apply_ite_of_true

added theorem Finset.prod_attach

added theorem Finset.prod_bij'

added theorem Finset.prod_bij

added theorem Finset.prod_bij_ne_one

added theorem Finset.prod_boole

added theorem Finset.prod_bunionᵢ

added theorem Finset.prod_cancels_of_partition_cancels

added theorem Finset.prod_coe_sort

added theorem Finset.prod_coe_sort_eq_attach

added theorem Finset.prod_comm'

added theorem Finset.prod_comm

added theorem Finset.prod_comp

added theorem Finset.prod_compl_mul_prod

added theorem Finset.prod_congr

added theorem Finset.prod_congr_set

added theorem Finset.prod_cons

added theorem Finset.prod_const

added theorem Finset.prod_const_one

added theorem Finset.prod_disjUnion

added theorem Finset.prod_disjUnionᵢ

added theorem Finset.prod_disj_sum

added theorem Finset.prod_dite

added theorem Finset.prod_dite_eq'

added theorem Finset.prod_dite_eq

added theorem Finset.prod_dite_irrel

added theorem Finset.prod_dite_of_false

added theorem Finset.prod_dite_of_true

added theorem Finset.prod_div_distrib

added theorem Finset.prod_dvd_prod_of_dvd

added theorem Finset.prod_dvd_prod_of_subset

added theorem Finset.prod_empty

added theorem Finset.prod_eq_fold

added theorem Finset.prod_eq_mul

added theorem Finset.prod_eq_mul_of_mem

added theorem Finset.prod_eq_mul_prod_diff_singleton

added theorem Finset.prod_eq_multiset_prod

added theorem Finset.prod_eq_one

added theorem Finset.prod_eq_prod_diff_singleton_mul

added theorem Finset.prod_eq_single

added theorem Finset.prod_eq_single_of_mem

added theorem Finset.prod_eq_zero

added theorem Finset.prod_eq_zero_iff

added theorem Finset.prod_erase

added theorem Finset.prod_erase_eq_div

added theorem Finset.prod_erase_mul

added theorem Finset.prod_extend_by_one

added theorem Finset.prod_fiberwise_of_maps_to

added theorem Finset.prod_filter

added theorem Finset.prod_filter_mul_prod_filter_not

added theorem Finset.prod_filter_ne_one

added theorem Finset.prod_filter_of_ne

added theorem Finset.prod_finset_coe

added theorem Finset.prod_finset_product'

added theorem Finset.prod_finset_product

added theorem Finset.prod_finset_product_right'

added theorem Finset.prod_finset_product_right

added theorem Finset.prod_flip

added theorem Finset.prod_hom_rel

added theorem Finset.prod_image'

added theorem Finset.prod_image

added theorem Finset.prod_induction

added theorem Finset.prod_induction_nonempty

added theorem Finset.prod_insert

added theorem Finset.prod_insert_of_eq_one_if_not_mem

added theorem Finset.prod_insert_one

added theorem Finset.prod_inter_mul_prod_diff

added theorem Finset.prod_inv_distrib

added theorem Finset.prod_involution

added theorem Finset.prod_ite

added theorem Finset.prod_ite_eq'

added theorem Finset.prod_ite_eq

added theorem Finset.prod_ite_index

added theorem Finset.prod_ite_irrel

added theorem Finset.prod_ite_mem

added theorem Finset.prod_ite_of_false

added theorem Finset.prod_ite_of_true

added theorem Finset.prod_ite_one

added theorem Finset.prod_list_count

added theorem Finset.prod_list_count_of_subset

added theorem Finset.prod_list_map_count

added theorem Finset.prod_map

added theorem Finset.prod_mem_multiset

added theorem Finset.prod_mk

added theorem Finset.prod_mul_distrib

added theorem Finset.prod_mul_prod_compl

added theorem Finset.prod_multiset_count

added theorem Finset.prod_multiset_count_of_subset

added theorem Finset.prod_multiset_map_count

added theorem Finset.prod_ne_zero_iff

added theorem Finset.prod_of_empty

added theorem Finset.prod_pair

added theorem Finset.prod_partition

added theorem Finset.prod_piecewise

added theorem Finset.prod_pow

added theorem Finset.prod_pow_boole

added theorem Finset.prod_product'

added theorem Finset.prod_product

added theorem Finset.prod_product_right'

added theorem Finset.prod_product_right

added theorem Finset.prod_range_add

added theorem Finset.prod_range_add_div_prod_range

added theorem Finset.prod_range_div'

added theorem Finset.prod_range_div

added theorem Finset.prod_range_induction

added theorem Finset.prod_range_one

added theorem Finset.prod_range_succ'

added theorem Finset.prod_range_succ

added theorem Finset.prod_range_succ_comm

added theorem Finset.prod_range_zero

added theorem Finset.prod_sdiff

added theorem Finset.prod_sdiff_div_prod_sdiff

added theorem Finset.prod_sdiff_eq_div

added theorem Finset.prod_sigma'

added theorem Finset.prod_sigma

added theorem Finset.prod_singleton

added theorem Finset.prod_subset

added theorem Finset.prod_subset_one_on_sdiff

added theorem Finset.prod_subtype

added theorem Finset.prod_subtype_eq_prod_filter

added theorem Finset.prod_subtype_map_embedding

added theorem Finset.prod_subtype_of_mem

added theorem Finset.prod_sum_elim

added theorem Finset.prod_to_list

added theorem Finset.prod_union

added theorem Finset.prod_union_inter

added theorem Finset.prod_unique_nonempty

added theorem Finset.prod_update_of_mem

added theorem Finset.prod_update_of_not_mem

added theorem Finset.prod_val

added theorem Finset.prod_zpow

added theorem Finset.sum_boole

added theorem Finset.sum_const_nat

added theorem Finset.sum_erase_lt_of_pos

added theorem Finset.sum_filter_count_eq_countp

added theorem Finset.sum_multiset_singleton

added theorem Finset.sum_pi_single'

added theorem Finset.sum_pi_single

added theorem Finset.sum_range_tsub

added theorem Finset.unop_sum

added theorem Fintype.prod_bijective

added theorem Fintype.prod_empty

added theorem Fintype.prod_eq_mul_prod_compl

added theorem Fintype.prod_eq_prod_compl_mul

added theorem Fintype.prod_equiv

added theorem Fintype.prod_subsingleton

added theorem Fintype.prod_subtype_mul_prod_subtype

added theorem Fintype.prod_unique

added theorem Int.cast_list_prod

added theorem Int.cast_list_sum

added theorem Int.cast_multiset_prod

added theorem Int.cast_multiset_sum

added theorem Int.cast_prod

added theorem Int.cast_sum

added theorem IsCompl.prod_mul_prod

added theorem List.prod_toFinset

added theorem MonoidHom.coe_finset_prod

added theorem MonoidHom.finset_prod_apply

added theorem Multiset.add_eq_union_left_of_le

added theorem Multiset.add_eq_union_right_of_le

added theorem Multiset.count_sum'

added theorem Multiset.disjoint_finset_sum_left

added theorem Multiset.disjoint_finset_sum_right

added theorem Multiset.disjoint_list_sum_left

added theorem Multiset.disjoint_list_sum_right

added theorem Multiset.disjoint_sum_left

added theorem Multiset.disjoint_sum_right

added theorem Multiset.exists_smul_of_dvd_count

added theorem Multiset.finset_sum_eq_sup_iff_disjoint

added theorem Multiset.prod_sum

added theorem Multiset.sup_powerset_len

added theorem Multiset.toFinset_prod_dvd_prod

added theorem Multiset.toFinset_sum_count_eq

added theorem Multiset.toFinset_sum_count_nsmul_eq

added theorem Nat.cast_list_prod

added theorem Nat.cast_list_sum

added theorem Nat.cast_multiset_prod

added theorem Nat.cast_multiset_sum

added theorem Nat.cast_prod

added theorem Nat.cast_sum

added theorem Units.coe_prod

added theorem Units.mk0_prod

added theorem map_prod

added theorem nat_abs_sum_le

added theorem ofAdd_list_prod

added theorem ofAdd_multiset_prod

added theorem ofAdd_sum

added theorem ofMul_list_prod

added theorem ofMul_multiset_prod

added theorem ofMul_prod

added theorem toAdd_list_sum

added theorem toAdd_multiset_sum

added theorem toAdd_prod

added theorem toMul_list_sum

added theorem toMul_multiset_sum

added theorem toMul_sum

Modified Mathlib/Data/Finset/Sum.lean

added theorem Finset.map_inl_disjUnion_map_inr

deleted theorem Finset.map_inl_disj_union_map_inr