gistfile1.txt

1393c1393
< add_equiv.map_sum: algebra/big_operators.lean
---
> add_equiv.map_sum: algebra/big_operators/basic.lean
1831c1831
< add_monoid_hom.map_sum: algebra/big_operators.lean
---
> add_monoid_hom.map_sum: algebra/big_operators/basic.lean
14853c14853
< directed.finset_le: algebra/big_operators.lean
---
> directed.finset_le: data/finset/order.lean
19745c19745
< finset.abs_sum_le_sum_abs: algebra/big_operators.lean
---
> finset.abs_sum_le_sum_abs: algebra/big_operators/order.lean
19787,19788c19787,19788
< finset.card_bind: algebra/big_operators.lean
< finset.card_bind_le: algebra/big_operators.lean
---
> finset.card_bind: algebra/big_operators/basic.lean
> finset.card_bind_le: algebra/big_operators/basic.lean
19796,19797c19796,19797
< finset.card_eq_sum_card_image: algebra/big_operators.lean
< finset.card_eq_sum_ones: algebra/big_operators.lean
---
> finset.card_eq_sum_card_image: algebra/big_operators/basic.lean
> finset.card_eq_sum_ones: algebra/big_operators/basic.lean
19810c19810
< finset.card_le_mul_card_image: algebra/big_operators.lean
---
> finset.card_le_mul_card_image: algebra/big_operators/order.lean
19819c19819
< finset.card_pi: algebra/big_operators.lean
---
> finset.card_pi: data/fintype/card.lean
19826c19826
< finset.card_sigma: algebra/big_operators.lean
---
> finset.card_sigma: algebra/big_operators/basic.lean
19910c19910
< finset.dvd_sum: algebra/big_operators.lean
---
> finset.dvd_sum: algebra/big_operators/ring.lean
19922,19923c19922,19923
< finset.eq_of_card_le_one_of_prod_eq: algebra/big_operators.lean
< finset.eq_of_card_le_one_of_sum_eq: algebra/big_operators.lean
---
> finset.eq_of_card_le_one_of_prod_eq: algebra/big_operators/basic.lean
> finset.eq_of_card_le_one_of_sum_eq: algebra/big_operators/basic.lean
19927c19927
< finset.eq_one_of_prod_eq_one: algebra/big_operators.lean
---
> finset.eq_one_of_prod_eq_one: algebra/big_operators/basic.lean
19930c19930
< finset.eq_zero_of_sum_eq_zero: algebra/big_operators.lean
---
> finset.eq_zero_of_sum_eq_zero: algebra/big_operators/basic.lean
19941,19942d19940
< finset.exists_card_smul_ge_sum: algebra/module.lean
< finset.exists_card_smul_le_sum: algebra/module.lean
19944,19945c19942,19943
< finset.exists_le: algebra/big_operators.lean
< finset.exists_le_of_sum_le: algebra/big_operators.lean
---
> finset.exists_le: data/finset/order.lean
> finset.exists_le_of_sum_le: algebra/big_operators/order.lean
19951,19953c19949,19951
< finset.exists_ne_one_of_prod_ne_one: algebra/big_operators.lean
< finset.exists_ne_zero_of_sum_ne_zero: algebra/big_operators.lean
< finset.exists_pos_of_sum_zero_of_exists_nonzero: algebra/big_operators.lean
---
> finset.exists_ne_one_of_prod_ne_one: algebra/big_operators/basic.lean
> finset.exists_ne_zero_of_sum_ne_zero: algebra/big_operators/basic.lean
> finset.exists_pos_of_sum_zero_of_exists_nonzero: algebra/big_operators/order.lean
20009c20007
< finset.gsmul_sum: algebra/big_operators.lean
---
> finset.gsmul_sum: algebra/big_operators/basic.lean
20133c20131
< finset.le_sum_of_subadditive: algebra/big_operators.lean
---
> finset.le_sum_of_subadditive: algebra/big_operators/order.lean
20250c20248
< finset.mul_sum: algebra/big_operators.lean
---
> finset.mul_sum: algebra/big_operators/ring.lean
20269,20270c20267,20268
< finset.nonempty_of_prod_ne_one: algebra/big_operators.lean
< finset.nonempty_of_sum_ne_zero: algebra/big_operators.lean
---
> finset.nonempty_of_prod_ne_one: algebra/big_operators/basic.lean
> finset.nonempty_of_sum_ne_zero: algebra/big_operators/basic.lean
20309,20317c20307,20315
< finset.prod: algebra/big_operators.lean
< finset.prod_Ico_add: algebra/big_operators.lean
< finset.prod_Ico_consecutive: algebra/big_operators.lean
< finset.prod_Ico_eq_mul_inv: algebra/big_operators.lean
< finset.prod_Ico_eq_prod_range: algebra/big_operators.lean
< finset.prod_Ico_id_eq_fact: algebra/big_operators.lean
< finset.prod_Ico_reflect: algebra/big_operators.lean
< finset.prod_Ico_succ_top: algebra/big_operators.lean
< finset.prod_add: algebra/big_operators.lean
---
> finset.prod: algebra/big_operators/basic.lean
> finset.prod_Ico_add: algebra/big_operators/intervals.lean
> finset.prod_Ico_consecutive: algebra/big_operators/intervals.lean
> finset.prod_Ico_eq_mul_inv: algebra/big_operators/intervals.lean
> finset.prod_Ico_eq_prod_range: algebra/big_operators/intervals.lean
> finset.prod_Ico_id_eq_fact: algebra/big_operators/intervals.lean
> finset.prod_Ico_reflect: algebra/big_operators/intervals.lean
> finset.prod_Ico_succ_top: algebra/big_operators/intervals.lean
> finset.prod_add: algebra/big_operators/ring.lean
20319,20321c20317,20319
< finset.prod_apply_dite: algebra/big_operators.lean
< finset.prod_apply_ite: algebra/big_operators.lean
< finset.prod_attach: algebra/big_operators.lean
---
> finset.prod_apply_dite: algebra/big_operators/basic.lean
> finset.prod_apply_ite: algebra/big_operators/basic.lean
> finset.prod_attach: algebra/big_operators/basic.lean
20323,20335c20321,20333
< finset.prod_bij': algebra/big_operators.lean
< finset.prod_bij: algebra/big_operators.lean
< finset.prod_bij_ne_one: algebra/big_operators.lean
< finset.prod_bind: algebra/big_operators.lean
< finset.prod_cancels_of_partition_cancels: algebra/big_operators.lean
< finset.prod_comm: algebra/big_operators.lean
< finset.prod_comp: algebra/big_operators.lean
< finset.prod_congr: algebra/big_operators.lean
< finset.prod_const: algebra/big_operators.lean
< finset.prod_const_one: algebra/big_operators.lean
< finset.prod_dite: algebra/big_operators.lean
< finset.prod_dite_eq': algebra/big_operators.lean
< finset.prod_dite_eq: algebra/big_operators.lean
---
> finset.prod_bij': algebra/big_operators/basic.lean
> finset.prod_bij: algebra/big_operators/basic.lean
> finset.prod_bij_ne_one: algebra/big_operators/basic.lean
> finset.prod_bind: algebra/big_operators/basic.lean
> finset.prod_cancels_of_partition_cancels: algebra/big_operators/basic.lean
> finset.prod_comm: algebra/big_operators/basic.lean
> finset.prod_comp: algebra/big_operators/basic.lean
> finset.prod_congr: algebra/big_operators/basic.lean
> finset.prod_const: algebra/big_operators/basic.lean
> finset.prod_const_one: algebra/big_operators/basic.lean
> finset.prod_dite: algebra/big_operators/basic.lean
> finset.prod_dite_eq': algebra/big_operators/basic.lean
> finset.prod_dite_eq: algebra/big_operators/basic.lean
20337,20344c20335,20342
< finset.prod_empty: algebra/big_operators.lean
< finset.prod_eq_fold: algebra/big_operators.lean
< finset.prod_eq_multiset_prod: algebra/big_operators.lean
< finset.prod_eq_one: algebra/big_operators.lean
< finset.prod_eq_prod_Ico_succ_bot: algebra/big_operators.lean
< finset.prod_eq_single: algebra/big_operators.lean
< finset.prod_eq_zero: algebra/big_operators.lean
< finset.prod_eq_zero_iff: algebra/big_operators.lean
---
> finset.prod_empty: algebra/big_operators/basic.lean
> finset.prod_eq_fold: algebra/big_operators/basic.lean
> finset.prod_eq_multiset_prod: algebra/big_operators/basic.lean
> finset.prod_eq_one: algebra/big_operators/basic.lean
> finset.prod_eq_prod_Ico_succ_bot: algebra/big_operators/intervals.lean
> finset.prod_eq_single: algebra/big_operators/basic.lean
> finset.prod_eq_zero: algebra/big_operators/basic.lean
> finset.prod_eq_zero_iff: algebra/big_operators/basic.lean
20346,20347c20344,20345
< finset.prod_erase: algebra/big_operators.lean
< finset.prod_extend_by_one: algebra/big_operators.lean
---
> finset.prod_erase: algebra/big_operators/basic.lean
> finset.prod_extend_by_one: algebra/big_operators/basic.lean
20349,20368c20347,20366
< finset.prod_filter: algebra/big_operators.lean
< finset.prod_filter_ne_one: algebra/big_operators.lean
< finset.prod_filter_of_ne: algebra/big_operators.lean
< finset.prod_flip: algebra/big_operators.lean
< finset.prod_hom: algebra/big_operators.lean
< finset.prod_hom_rel: algebra/big_operators.lean
< finset.prod_image': algebra/big_operators.lean
< finset.prod_image: algebra/big_operators.lean
< finset.prod_induction: algebra/big_operators.lean
< finset.prod_insert: algebra/big_operators.lean
< finset.prod_insert_of_eq_one_if_not_mem: algebra/big_operators.lean
< finset.prod_insert_one: algebra/big_operators.lean
< finset.prod_inv_distrib: algebra/big_operators.lean
< finset.prod_involution: algebra/big_operators.lean
< finset.prod_ite: algebra/big_operators.lean
< finset.prod_ite_eq': algebra/big_operators.lean
< finset.prod_ite_eq: algebra/big_operators.lean
< finset.prod_le_prod': algebra/big_operators.lean
< finset.prod_le_prod: algebra/big_operators.lean
< finset.prod_map: algebra/big_operators.lean
---
> finset.prod_filter: algebra/big_operators/basic.lean
> finset.prod_filter_ne_one: algebra/big_operators/basic.lean
> finset.prod_filter_of_ne: algebra/big_operators/basic.lean
> finset.prod_flip: algebra/big_operators/basic.lean
> finset.prod_hom: algebra/big_operators/basic.lean
> finset.prod_hom_rel: algebra/big_operators/basic.lean
> finset.prod_image': algebra/big_operators/basic.lean
> finset.prod_image: algebra/big_operators/basic.lean
> finset.prod_induction: algebra/big_operators/basic.lean
> finset.prod_insert: algebra/big_operators/basic.lean
> finset.prod_insert_of_eq_one_if_not_mem: algebra/big_operators/basic.lean
> finset.prod_insert_one: algebra/big_operators/basic.lean
> finset.prod_inv_distrib: algebra/big_operators/basic.lean
> finset.prod_involution: algebra/big_operators/basic.lean
> finset.prod_ite: algebra/big_operators/basic.lean
> finset.prod_ite_eq': algebra/big_operators/basic.lean
> finset.prod_ite_eq: algebra/big_operators/basic.lean
> finset.prod_le_prod': algebra/big_operators/order.lean
> finset.prod_le_prod: algebra/big_operators/order.lean
> finset.prod_map: algebra/big_operators/basic.lean
20371,20376c20369,20374
< finset.prod_mul_distrib: algebra/big_operators.lean
< finset.prod_multiset_count: algebra/big_operators.lean
< finset.prod_nat_cast: algebra/big_operators.lean
< finset.prod_nat_pow: algebra/big_operators.lean
< finset.prod_ne_zero_iff: algebra/big_operators.lean
< finset.prod_nonneg: algebra/big_operators.lean
---
> finset.prod_mul_distrib: algebra/big_operators/basic.lean
> finset.prod_multiset_count: algebra/big_operators/basic.lean
> finset.prod_nat_cast: algebra/big_operators/ring.lean
> finset.prod_nat_pow: algebra/big_operators/basic.lean
> finset.prod_ne_zero_iff: algebra/big_operators/basic.lean
> finset.prod_nonneg: algebra/big_operators/order.lean
20378,20384c20376,20382
< finset.prod_pair: algebra/big_operators.lean
< finset.prod_piecewise: algebra/big_operators.lean
< finset.prod_pos: algebra/big_operators.lean
< finset.prod_pow: algebra/big_operators.lean
< finset.prod_pow_boole: algebra/big_operators.lean
< finset.prod_pow_eq_pow_sum: algebra/big_operators.lean
< finset.prod_powerset_insert: algebra/big_operators.lean
---
> finset.prod_pair: algebra/big_operators/basic.lean
> finset.prod_piecewise: algebra/big_operators/basic.lean
> finset.prod_pos: algebra/big_operators/order.lean
> finset.prod_pow: algebra/big_operators/basic.lean
> finset.prod_pow_boole: algebra/big_operators/basic.lean
> finset.prod_pow_eq_pow_sum: algebra/big_operators/ring.lean
> finset.prod_powerset_insert: algebra/big_operators/ring.lean
20387,20401c20385,20399
< finset.prod_product': algebra/big_operators.lean
< finset.prod_product: algebra/big_operators.lean
< finset.prod_range_div': algebra/big_operators.lean
< finset.prod_range_div: algebra/big_operators.lean
< finset.prod_range_induction: algebra/big_operators.lean
< finset.prod_range_mul_prod_Ico: algebra/big_operators.lean
< finset.prod_range_one: algebra/big_operators.lean
< finset.prod_range_reflect: algebra/big_operators.lean
< finset.prod_range_succ': algebra/big_operators.lean
< finset.prod_range_succ: algebra/big_operators.lean
< finset.prod_range_zero: algebra/big_operators.lean
< finset.prod_sdiff: algebra/big_operators.lean
< finset.prod_sigma: algebra/big_operators.lean
< finset.prod_singleton: algebra/big_operators.lean
< finset.prod_subset: algebra/big_operators.lean
---
> finset.prod_product': algebra/big_operators/basic.lean
> finset.prod_product: algebra/big_operators/basic.lean
> finset.prod_range_div': algebra/big_operators/basic.lean
> finset.prod_range_div: algebra/big_operators/basic.lean
> finset.prod_range_induction: algebra/big_operators/basic.lean
> finset.prod_range_mul_prod_Ico: algebra/big_operators/intervals.lean
> finset.prod_range_one: algebra/big_operators/basic.lean
> finset.prod_range_reflect: algebra/big_operators/intervals.lean
> finset.prod_range_succ': algebra/big_operators/basic.lean
> finset.prod_range_succ: algebra/big_operators/basic.lean
> finset.prod_range_zero: algebra/big_operators/basic.lean
> finset.prod_sdiff: algebra/big_operators/basic.lean
> finset.prod_sigma: algebra/big_operators/basic.lean
> finset.prod_singleton: algebra/big_operators/basic.lean
> finset.prod_subset: algebra/big_operators/basic.lean
20403,20409c20401,20407
< finset.prod_subtype_eq_prod_filter: algebra/big_operators.lean
< finset.prod_subtype_map_embedding: algebra/big_operators.lean
< finset.prod_subtype_of_mem: algebra/big_operators.lean
< finset.prod_sum: algebra/big_operators.lean
< finset.prod_sum_elim: algebra/big_operators.lean
< finset.prod_union: algebra/big_operators.lean
< finset.prod_union_inter: algebra/big_operators.lean
---
> finset.prod_subtype_eq_prod_filter: algebra/big_operators/basic.lean
> finset.prod_subtype_map_embedding: algebra/big_operators/basic.lean
> finset.prod_subtype_of_mem: algebra/big_operators/basic.lean
> finset.prod_sum: algebra/big_operators/ring.lean
> finset.prod_sum_elim: algebra/big_operators/basic.lean
> finset.prod_union: algebra/big_operators/basic.lean
> finset.prod_union_inter: algebra/big_operators/basic.lean
20412,20413c20410,20411
< finset.prod_update_of_mem: algebra/big_operators.lean
< finset.prod_update_of_not_mem: algebra/big_operators.lean
---
> finset.prod_update_of_mem: algebra/big_operators/basic.lean
> finset.prod_update_of_not_mem: algebra/big_operators/basic.lean
20463c20461
< finset.single_le_sum: algebra/big_operators.lean
---
> finset.single_le_sum: algebra/big_operators/order.lean
20512,20520c20510,20518
< finset.sum: algebra/big_operators.lean
< finset.sum_Ico_add: algebra/big_operators.lean
< finset.sum_Ico_consecutive: algebra/big_operators.lean
< finset.sum_Ico_eq_add_neg: algebra/big_operators.lean
< finset.sum_Ico_eq_sub: algebra/big_operators.lean
< finset.sum_Ico_eq_sum_range: algebra/big_operators.lean
< finset.sum_Ico_reflect: algebra/big_operators.lean
< finset.sum_Ico_succ_top: algebra/big_operators.lean
< finset.sum_add_distrib: algebra/big_operators.lean
---
> finset.sum: algebra/big_operators/basic.lean
> finset.sum_Ico_add: algebra/big_operators/intervals.lean
> finset.sum_Ico_consecutive: algebra/big_operators/intervals.lean
> finset.sum_Ico_eq_add_neg: algebra/big_operators/intervals.lean
> finset.sum_Ico_eq_sub: algebra/big_operators/intervals.lean
> finset.sum_Ico_eq_sum_range: algebra/big_operators/intervals.lean
> finset.sum_Ico_reflect: algebra/big_operators/intervals.lean
> finset.sum_Ico_succ_top: algebra/big_operators/intervals.lean
> finset.sum_add_distrib: algebra/big_operators/basic.lean
20522,20524c20520,20522
< finset.sum_apply_dite: algebra/big_operators.lean
< finset.sum_apply_ite: algebra/big_operators.lean
< finset.sum_attach: algebra/big_operators.lean
---
> finset.sum_apply_dite: algebra/big_operators/basic.lean
> finset.sum_apply_ite: algebra/big_operators/basic.lean
> finset.sum_attach: algebra/big_operators/basic.lean
20526,20552c20524,20549
< finset.sum_bij': algebra/big_operators.lean
< finset.sum_bij: algebra/big_operators.lean
< finset.sum_bij_ne_zero: algebra/big_operators.lean
< finset.sum_bind: algebra/big_operators.lean
< finset.sum_boole: algebra/big_operators.lean
< finset.sum_boole_mul: algebra/big_operators.lean
< finset.sum_cancels_of_partition_cancels: algebra/big_operators.lean
< finset.sum_comm: algebra/big_operators.lean
< finset.sum_comp: algebra/big_operators.lean
< finset.sum_congr: algebra/big_operators.lean
< finset.sum_const': algebra/module.lean
< finset.sum_const: algebra/big_operators.lean
< finset.sum_const_nat: algebra/big_operators.lean
< finset.sum_const_zero: algebra/big_operators.lean
< finset.sum_dite: algebra/big_operators.lean
< finset.sum_dite_eq': algebra/big_operators.lean
< finset.sum_dite_eq: algebra/big_operators.lean
< finset.sum_div: algebra/big_operators.lean
< finset.sum_empty: algebra/big_operators.lean
< finset.sum_eq_fold: algebra/big_operators.lean
< finset.sum_eq_multiset_sum: algebra/big_operators.lean
< finset.sum_eq_single: algebra/big_operators.lean
< finset.sum_eq_sum_Ico_succ_bot: algebra/big_operators.lean
< finset.sum_eq_zero: algebra/big_operators.lean
< finset.sum_eq_zero_iff: algebra/big_operators.lean
< finset.sum_eq_zero_iff_of_nonneg: algebra/big_operators.lean
< finset.sum_eq_zero_iff_of_nonpos: algebra/big_operators.lean
---
> finset.sum_bij': algebra/big_operators/basic.lean
> finset.sum_bij: algebra/big_operators/basic.lean
> finset.sum_bij_ne_zero: algebra/big_operators/basic.lean
> finset.sum_bind: algebra/big_operators/basic.lean
> finset.sum_boole: algebra/big_operators/basic.lean
> finset.sum_boole_mul: algebra/big_operators/ring.lean
> finset.sum_cancels_of_partition_cancels: algebra/big_operators/basic.lean
> finset.sum_comm: algebra/big_operators/basic.lean
> finset.sum_comp: algebra/big_operators/basic.lean
> finset.sum_congr: algebra/big_operators/basic.lean
> finset.sum_const: algebra/big_operators/basic.lean
> finset.sum_const_nat: algebra/big_operators/basic.lean
> finset.sum_const_zero: algebra/big_operators/basic.lean
> finset.sum_dite: algebra/big_operators/basic.lean
> finset.sum_dite_eq': algebra/big_operators/basic.lean
> finset.sum_dite_eq: algebra/big_operators/basic.lean
> finset.sum_div: algebra/big_operators/ring.lean
> finset.sum_empty: algebra/big_operators/basic.lean
> finset.sum_eq_fold: algebra/big_operators/basic.lean
> finset.sum_eq_multiset_sum: algebra/big_operators/basic.lean
> finset.sum_eq_single: algebra/big_operators/basic.lean
> finset.sum_eq_sum_Ico_succ_bot: algebra/big_operators/intervals.lean
> finset.sum_eq_zero: algebra/big_operators/basic.lean
> finset.sum_eq_zero_iff: algebra/big_operators/order.lean
> finset.sum_eq_zero_iff_of_nonneg: algebra/big_operators/order.lean
> finset.sum_eq_zero_iff_of_nonpos: algebra/big_operators/order.lean
20554,20555c20551,20552
< finset.sum_erase: algebra/big_operators.lean
< finset.sum_extend_by_zero: algebra/big_operators.lean
---
> finset.sum_erase: algebra/big_operators/basic.lean
> finset.sum_extend_by_zero: algebra/big_operators/basic.lean
20557,20595c20554,20591
< finset.sum_filter: algebra/big_operators.lean
< finset.sum_filter_ne_zero: algebra/big_operators.lean
< finset.sum_filter_of_ne: algebra/big_operators.lean
< finset.sum_flip: algebra/big_operators.lean
< finset.sum_hom: algebra/big_operators.lean
< finset.sum_hom_rel: algebra/big_operators.lean
< finset.sum_image': algebra/big_operators.lean
< finset.sum_image: algebra/big_operators.lean
< finset.sum_induction: algebra/big_operators.lean
< finset.sum_insert: algebra/big_operators.lean
< finset.sum_insert_of_eq_zero_if_not_mem: algebra/big_operators.lean
< finset.sum_insert_zero: algebra/big_operators.lean
< finset.sum_involution: algebra/big_operators.lean
< finset.sum_ite: algebra/big_operators.lean
< finset.sum_ite_eq': algebra/big_operators.lean
< finset.sum_ite_eq: algebra/big_operators.lean
< finset.sum_le_sum: algebra/big_operators.lean
< finset.sum_le_sum_of_ne_zero: algebra/big_operators.lean
< finset.sum_le_sum_of_subset: algebra/big_operators.lean
< finset.sum_le_sum_of_subset_of_nonneg: algebra/big_operators.lean
< finset.sum_lt_sum: algebra/big_operators.lean
< finset.sum_lt_sum_of_nonempty: algebra/big_operators.lean
< finset.sum_lt_sum_of_subset: algebra/big_operators.lean
< finset.sum_map: algebra/big_operators.lean
< finset.sum_mono_set: algebra/big_operators.lean
< finset.sum_mono_set_of_nonneg: algebra/big_operators.lean
< finset.sum_mul: algebra/big_operators.lean
< finset.sum_mul_boole: algebra/big_operators.lean
< finset.sum_mul_sum: algebra/big_operators.lean
< finset.sum_nat_cast: algebra/big_operators.lean
< finset.sum_nat_coe_enat: algebra/big_operators.lean
< finset.sum_neg_distrib: algebra/big_operators.lean
< finset.sum_nonneg: algebra/big_operators.lean
< finset.sum_nonpos: algebra/big_operators.lean
< finset.sum_nsmul: algebra/big_operators.lean
< finset.sum_pair: algebra/big_operators.lean
< finset.sum_piecewise: algebra/big_operators.lean
< finset.sum_pow_mul_eq_add_pow: algebra/big_operators.lean
< finset.sum_powerset_insert: algebra/big_operators.lean
---
> finset.sum_filter: algebra/big_operators/basic.lean
> finset.sum_filter_ne_zero: algebra/big_operators/basic.lean
> finset.sum_filter_of_ne: algebra/big_operators/basic.lean
> finset.sum_flip: algebra/big_operators/basic.lean
> finset.sum_hom: algebra/big_operators/basic.lean
> finset.sum_hom_rel: algebra/big_operators/basic.lean
> finset.sum_image': algebra/big_operators/basic.lean
> finset.sum_image: algebra/big_operators/basic.lean
> finset.sum_induction: algebra/big_operators/basic.lean
> finset.sum_insert: algebra/big_operators/basic.lean
> finset.sum_insert_of_eq_zero_if_not_mem: algebra/big_operators/basic.lean
> finset.sum_insert_zero: algebra/big_operators/basic.lean
> finset.sum_involution: algebra/big_operators/basic.lean
> finset.sum_ite: algebra/big_operators/basic.lean
> finset.sum_ite_eq': algebra/big_operators/basic.lean
> finset.sum_ite_eq: algebra/big_operators/basic.lean
> finset.sum_le_sum: algebra/big_operators/order.lean
> finset.sum_le_sum_of_ne_zero: algebra/big_operators/order.lean
> finset.sum_le_sum_of_subset: algebra/big_operators/order.lean
> finset.sum_le_sum_of_subset_of_nonneg: algebra/big_operators/order.lean
> finset.sum_lt_sum: algebra/big_operators/order.lean
> finset.sum_lt_sum_of_nonempty: algebra/big_operators/order.lean
> finset.sum_lt_sum_of_subset: algebra/big_operators/order.lean
> finset.sum_map: algebra/big_operators/basic.lean
> finset.sum_mono_set: algebra/big_operators/order.lean
> finset.sum_mono_set_of_nonneg: algebra/big_operators/order.lean
> finset.sum_mul: algebra/big_operators/ring.lean
> finset.sum_mul_boole: algebra/big_operators/ring.lean
> finset.sum_mul_sum: algebra/big_operators/ring.lean
> finset.sum_nat_cast: algebra/big_operators/basic.lean
> finset.sum_neg_distrib: algebra/big_operators/basic.lean
> finset.sum_nonneg: algebra/big_operators/order.lean
> finset.sum_nonpos: algebra/big_operators/order.lean
> finset.sum_nsmul: algebra/big_operators/basic.lean
> finset.sum_pair: algebra/big_operators/basic.lean
> finset.sum_piecewise: algebra/big_operators/basic.lean
> finset.sum_pow_mul_eq_add_pow: algebra/big_operators/ring.lean
> finset.sum_powerset_insert: algebra/big_operators/ring.lean
20598,20614c20594,20610
< finset.sum_product': algebra/big_operators.lean
< finset.sum_product: algebra/big_operators.lean
< finset.sum_range_add_sum_Ico: algebra/big_operators.lean
< finset.sum_range_id: algebra/big_operators.lean
< finset.sum_range_id_mul_two: algebra/big_operators.lean
< finset.sum_range_induction: algebra/big_operators.lean
< finset.sum_range_one: algebra/big_operators.lean
< finset.sum_range_reflect: algebra/big_operators.lean
< finset.sum_range_sub': algebra/big_operators.lean
< finset.sum_range_sub: algebra/big_operators.lean
< finset.sum_range_sub_of_monotone: algebra/big_operators.lean
< finset.sum_range_succ': algebra/big_operators.lean
< finset.sum_range_succ: algebra/big_operators.lean
< finset.sum_range_zero: algebra/big_operators.lean
< finset.sum_sdiff: algebra/big_operators.lean
< finset.sum_sigma: algebra/big_operators.lean
< finset.sum_singleton: algebra/big_operators.lean
---
> finset.sum_product': algebra/big_operators/basic.lean
> finset.sum_product: algebra/big_operators/basic.lean
> finset.sum_range_add_sum_Ico: algebra/big_operators/intervals.lean
> finset.sum_range_id: algebra/big_operators/intervals.lean
> finset.sum_range_id_mul_two: algebra/big_operators/intervals.lean
> finset.sum_range_induction: algebra/big_operators/basic.lean
> finset.sum_range_one: algebra/big_operators/basic.lean
> finset.sum_range_reflect: algebra/big_operators/intervals.lean
> finset.sum_range_sub': algebra/big_operators/basic.lean
> finset.sum_range_sub: algebra/big_operators/basic.lean
> finset.sum_range_sub_of_monotone: algebra/big_operators/basic.lean
> finset.sum_range_succ': algebra/big_operators/basic.lean
> finset.sum_range_succ: algebra/big_operators/basic.lean
> finset.sum_range_zero: algebra/big_operators/basic.lean
> finset.sum_sdiff: algebra/big_operators/basic.lean
> finset.sum_sigma: algebra/big_operators/basic.lean
> finset.sum_singleton: algebra/big_operators/basic.lean
20616,20617c20612,20613
< finset.sum_sub_distrib: algebra/big_operators.lean
< finset.sum_subset: algebra/big_operators.lean
---
> finset.sum_sub_distrib: algebra/big_operators/basic.lean
> finset.sum_subset: algebra/big_operators/basic.lean
20619,20624c20615,20620
< finset.sum_subtype_eq_sum_filter: algebra/big_operators.lean
< finset.sum_subtype_map_embedding: algebra/big_operators.lean
< finset.sum_subtype_of_mem: algebra/big_operators.lean
< finset.sum_sum_elim: algebra/big_operators.lean
< finset.sum_union: algebra/big_operators.lean
< finset.sum_union_inter: algebra/big_operators.lean
---
> finset.sum_subtype_eq_sum_filter: algebra/big_operators/basic.lean
> finset.sum_subtype_map_embedding: algebra/big_operators/basic.lean
> finset.sum_subtype_of_mem: algebra/big_operators/basic.lean
> finset.sum_sum_elim: algebra/big_operators/basic.lean
> finset.sum_union: algebra/big_operators/basic.lean
> finset.sum_union_inter: algebra/big_operators/basic.lean
20626,20627c20622,20623
< finset.sum_update_of_mem: algebra/big_operators.lean
< finset.sum_update_of_not_mem: algebra/big_operators.lean
---
> finset.sum_update_of_mem: algebra/big_operators/basic.lean
> finset.sum_update_of_not_mem: algebra/big_operators/basic.lean
21214a21211,21213
> foo.add_comm_group: linear_algebra/test.lean
> foo.module: linear_algebra/test.lean
> foo: linear_algebra/test.lean
27137d27135
< is_add_group_hom_finset_sum: algebra/big_operators.lean
27880d27877
< is_group_hom_finset_prod: algebra/big_operators.lean
30033d30029
< linarith.certificate_oracle: tactic/linarith/datatypes.lean
30176d30171
< linarith.linarith_config.oracle: tactic/linarith/datatypes.lean
36832c36827
< monoid_hom.map_prod: algebra/big_operators.lean
---
> monoid_hom.map_prod: algebra/big_operators/basic.lean
37124c37119
< mul_equiv.map_prod: algebra/big_operators.lean
---
> mul_equiv.map_prod: algebra/big_operators/basic.lean
38360c38355
< multiset.to_finset_sum_count_eq: algebra/big_operators.lean
---
> multiset.to_finset_sum_count_eq: algebra/big_operators/basic.lean
50246,50247c50241,50242
< ring_hom.map_list_prod: algebra/big_operators.lean
< ring_hom.map_list_sum: algebra/big_operators.lean
---
> ring_hom.map_list_prod: algebra/big_operators/basic.lean
> ring_hom.map_list_sum: algebra/big_operators/basic.lean
50253,50254c50248,50249
< ring_hom.map_multiset_prod: algebra/big_operators.lean
< ring_hom.map_multiset_sum: algebra/big_operators.lean
---
> ring_hom.map_multiset_prod: algebra/big_operators/basic.lean
> ring_hom.map_multiset_sum: algebra/big_operators/basic.lean
50261c50256
< ring_hom.map_prod: algebra/big_operators.lean
---
> ring_hom.map_prod: algebra/big_operators/basic.lean
50267c50262
< ring_hom.map_sum: algebra/big_operators.lean
---
> ring_hom.map_sum: algebra/big_operators/basic.lean
58411a58407
> tensor_power: linear_algebra/test.lean
62022c62018
< with_top.op_sum: algebra/big_operators.lean
---
> with_top.op_sum: algebra/big_operators/order.lean
62033,62035c62029,62031
< with_top.sum_eq_top_iff: algebra/big_operators.lean
< with_top.sum_lt_top: algebra/big_operators.lean
< with_top.sum_lt_top_iff: algebra/big_operators.lean
---
> with_top.sum_eq_top_iff: algebra/big_operators/order.lean
> with_top.sum_lt_top: algebra/big_operators/order.lean
> with_top.sum_lt_top_iff: algebra/big_operators/order.lean
62044c62040
< with_top.unop_sum: algebra/big_operators.lean
---
> with_top.unop_sum: algebra/big_operators/order.lean