Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-19 19:30 f9c30004

View on Github →

refactor(data/finsupp/basic): split data/finsupp/basic into three parts (#15699) This PR splits the ~2900 lines of data/finsupp/basic into more manageable parts:

  • the most basic material (~1000 lines) moves to data/finsupp/defs
  • lemmas about finsupp.sum and finsupp.prod move to algebra/big_operators/finsupp
  • the remaining less-used definitions and lemmas remain in data/finsupp/basic (~1600 lines)

Estimated changes

added theorem finsupp.coe_finset_sum
added theorem finsupp.coe_sum
added theorem finsupp.mul_prod_erase
added theorem finsupp.on_finset_prod
added def finsupp.prod
added theorem finsupp.prod_add_index
added theorem finsupp.prod_comm
added theorem finsupp.prod_congr
added theorem finsupp.prod_fintype
added theorem finsupp.prod_inv
added theorem finsupp.prod_ite_eq'
added theorem finsupp.prod_ite_eq
added theorem finsupp.prod_mul
added theorem finsupp.prod_neg_index
added theorem finsupp.prod_pow
added theorem finsupp.prod_sum_index
added theorem finsupp.single_sum
added theorem finsupp.sum_apply
added theorem finsupp.sum_single
added theorem finsupp.sum_sub
added theorem finsupp.sum_sub_index
added theorem finsupp.sum_zero
added theorem finsupp.support_sum
added theorem map_finsupp_prod
deleted theorem finsupp.add_apply
deleted theorem finsupp.add_hom_ext'
deleted theorem finsupp.add_hom_ext
deleted theorem finsupp.coe_add
deleted theorem finsupp.coe_eq_zero
deleted theorem finsupp.coe_finset_sum
deleted theorem finsupp.coe_fn_inj
deleted theorem finsupp.coe_fn_injective
deleted theorem finsupp.coe_mk
deleted theorem finsupp.coe_neg
deleted theorem finsupp.coe_sub
deleted theorem finsupp.coe_sum
deleted theorem finsupp.coe_update
deleted theorem finsupp.coe_zero
deleted theorem finsupp.comp_lift_add_hom
deleted theorem finsupp.congr_fun
deleted def finsupp.emb_domain
deleted theorem finsupp.emb_domain_add
deleted theorem finsupp.emb_domain_apply
deleted theorem finsupp.emb_domain_inj
deleted theorem finsupp.emb_domain_single
deleted theorem finsupp.emb_domain_zero
deleted theorem finsupp.eq_single_iff
deleted def finsupp.erase
deleted theorem finsupp.erase_add
deleted theorem finsupp.erase_add_single
deleted theorem finsupp.erase_ne
deleted theorem finsupp.erase_same
deleted theorem finsupp.erase_single
deleted theorem finsupp.erase_single_ne
deleted theorem finsupp.erase_zero
deleted theorem finsupp.ext
deleted theorem finsupp.ext_iff'
deleted theorem finsupp.ext_iff
deleted theorem finsupp.finite_support
deleted theorem finsupp.finset_sum_apply
deleted theorem finsupp.fun_support_eq
deleted theorem finsupp.induction_linear
deleted theorem finsupp.induction₂
deleted def finsupp.map_range
deleted theorem finsupp.map_range_add
deleted theorem finsupp.map_range_apply
deleted theorem finsupp.map_range_comp
deleted theorem finsupp.map_range_id
deleted theorem finsupp.map_range_single
deleted theorem finsupp.map_range_zero
deleted theorem finsupp.mem_support_iff
deleted theorem finsupp.mul_hom_ext'
deleted theorem finsupp.mul_hom_ext
deleted theorem finsupp.mul_prod_erase'
deleted theorem finsupp.mul_prod_erase
deleted theorem finsupp.multiset_map_sum
deleted theorem finsupp.multiset_sum_sum
deleted theorem finsupp.neg_apply
deleted def finsupp.on_finset
deleted theorem finsupp.on_finset_apply
deleted theorem finsupp.on_finset_prod
deleted def finsupp.prod
deleted theorem finsupp.prod_add_index'
deleted theorem finsupp.prod_add_index
deleted theorem finsupp.prod_comm
deleted theorem finsupp.prod_congr
deleted theorem finsupp.prod_emb_domain
deleted theorem finsupp.prod_fintype
deleted theorem finsupp.prod_inv
deleted theorem finsupp.prod_ite_eq'
deleted theorem finsupp.prod_ite_eq
deleted theorem finsupp.prod_mul
deleted theorem finsupp.prod_neg_index
deleted theorem finsupp.prod_pow
deleted theorem finsupp.prod_single_index
deleted theorem finsupp.prod_sum_index
deleted theorem finsupp.prod_zero_index
deleted def finsupp.single
deleted theorem finsupp.single_add
deleted theorem finsupp.single_add_erase
deleted theorem finsupp.single_apply
deleted theorem finsupp.single_apply_mem
deleted theorem finsupp.single_eq_of_ne
deleted theorem finsupp.single_eq_same
deleted theorem finsupp.single_eq_update
deleted theorem finsupp.single_eq_zero
deleted theorem finsupp.single_finset_sum
deleted theorem finsupp.single_injective
deleted theorem finsupp.single_left_inj
deleted theorem finsupp.single_sum
deleted theorem finsupp.single_swap
deleted theorem finsupp.single_zero
deleted theorem finsupp.sub_apply
deleted theorem finsupp.sum_apply
deleted theorem finsupp.sum_hom_add_index
deleted theorem finsupp.sum_ite_self_eq'
deleted theorem finsupp.sum_ite_self_eq
deleted theorem finsupp.sum_single
deleted theorem finsupp.sum_sub
deleted theorem finsupp.sum_sub_index
deleted theorem finsupp.sum_univ_single'
deleted theorem finsupp.sum_univ_single
deleted theorem finsupp.sum_zero
deleted theorem finsupp.support_add
deleted theorem finsupp.support_add_eq
deleted theorem finsupp.support_eq_empty
deleted theorem finsupp.support_erase
deleted theorem finsupp.support_map_range
deleted theorem finsupp.support_neg
deleted theorem finsupp.support_on_finset
deleted theorem finsupp.support_sub
deleted theorem finsupp.support_sum
deleted theorem finsupp.support_update
deleted theorem finsupp.support_zero
deleted theorem finsupp.support_zip_with
deleted theorem finsupp.unique_ext
deleted theorem finsupp.unique_ext_iff
deleted theorem finsupp.unique_single
deleted def finsupp.update
deleted theorem finsupp.update_self
deleted theorem finsupp.zero_apply
deleted theorem finsupp.zero_update
deleted def finsupp.zip_with
deleted theorem finsupp.zip_with_apply
deleted structure finsupp
deleted theorem map_finsupp_prod
added theorem finsupp.add_apply
added theorem finsupp.add_hom_ext'
added theorem finsupp.add_hom_ext
added theorem finsupp.coe_add
added theorem finsupp.coe_eq_zero
added theorem finsupp.coe_fn_inj
added theorem finsupp.coe_mk
added theorem finsupp.coe_neg
added theorem finsupp.coe_sub
added theorem finsupp.coe_update
added theorem finsupp.coe_zero
added theorem finsupp.congr_fun
added theorem finsupp.emb_domain_add
added theorem finsupp.emb_domain_inj
added theorem finsupp.eq_single_iff
added def finsupp.erase
added theorem finsupp.erase_add
added theorem finsupp.erase_ne
added theorem finsupp.erase_same
added theorem finsupp.erase_single
added theorem finsupp.erase_zero
added theorem finsupp.ext
added theorem finsupp.ext_iff'
added theorem finsupp.ext_iff
added theorem finsupp.finite_support
added theorem finsupp.fun_support_eq
added theorem finsupp.induction₂
added theorem finsupp.map_range_add
added theorem finsupp.map_range_comp
added theorem finsupp.map_range_id
added theorem finsupp.map_range_zero
added theorem finsupp.mul_hom_ext'
added theorem finsupp.mul_hom_ext
added theorem finsupp.neg_apply
added def finsupp.single
added theorem finsupp.single_add
added theorem finsupp.single_apply
added theorem finsupp.single_eq_same
added theorem finsupp.single_eq_zero
added theorem finsupp.single_swap
added theorem finsupp.single_zero
added theorem finsupp.sub_apply
added theorem finsupp.support_add
added theorem finsupp.support_add_eq
added theorem finsupp.support_erase
added theorem finsupp.support_neg
added theorem finsupp.support_sub
added theorem finsupp.support_update
added theorem finsupp.support_zero
added theorem finsupp.unique_ext
added theorem finsupp.unique_ext_iff
added theorem finsupp.unique_single
added def finsupp.update
added theorem finsupp.update_self
added theorem finsupp.zero_apply
added theorem finsupp.zero_update
added def finsupp.zip_with
added theorem finsupp.zip_with_apply
added structure finsupp