Commit 2023-01-27 17:15 9b757df6

View on Github →

feat: port Data.Dfinsupp.Basic (#1829)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Dfinsupp/Basic.lean

added theorem AddEquiv.map_dfinsupp_sumAddHom

added theorem AddMonoidHom.coe_dfinsupp_sumAddHom

added theorem AddMonoidHom.dfinsupp_sumAddHom_apply

added theorem AddMonoidHom.map_dfinsupp_sumAddHom

added theorem AddSubmonoid.bsupr_eq_mrange_dfinsupp_sumAddHom

added theorem AddSubmonoid.mem_bsupr_iff_exists_dfinsupp

added theorem AddSubmonoid.mem_supᵢ_iff_exists_dfinsupp'

added theorem AddSubmonoid.mem_supᵢ_iff_exists_dfinsupp

added theorem AddSubmonoid.supᵢ_eq_mrange_dfinsupp_sumAddHom

added theorem Dfinsupp.add_apply

added theorem Dfinsupp.add_closure_unionᵢ_range_single

added theorem Dfinsupp.add_hom_ext'

added theorem Dfinsupp.add_hom_ext

added def Dfinsupp.coeFnAddMonoidHom

added theorem Dfinsupp.coeFn_injective

added theorem Dfinsupp.coe_add

added theorem Dfinsupp.coe_finset_sum

added theorem Dfinsupp.coe_mk'

added theorem Dfinsupp.coe_neg

added theorem Dfinsupp.coe_nsmul

added theorem Dfinsupp.coe_piecewise

added theorem Dfinsupp.coe_smul

added theorem Dfinsupp.coe_sub

added theorem Dfinsupp.coe_update

added theorem Dfinsupp.coe_zero

added theorem Dfinsupp.coe_zsmul

added def Dfinsupp.comapDomain'

added theorem Dfinsupp.comapDomain'_add

added theorem Dfinsupp.comapDomain'_apply

added theorem Dfinsupp.comapDomain'_single

added theorem Dfinsupp.comapDomain'_smul

added theorem Dfinsupp.comapDomain'_zero

added theorem Dfinsupp.comapDomain_add

added theorem Dfinsupp.comapDomain_apply

added theorem Dfinsupp.comapDomain_single

added theorem Dfinsupp.comapDomain_smul

added theorem Dfinsupp.comapDomain_zero

added theorem Dfinsupp.comp_liftAddHom

added theorem Dfinsupp.comp_sumAddHom

added theorem Dfinsupp.eq_mk_support

added def Dfinsupp.equivCongrLeft

added def Dfinsupp.equivFunOnFintype

added theorem Dfinsupp.equivFunOnFintype_single

added theorem Dfinsupp.equivFunOnFintype_symm_coe

added theorem Dfinsupp.equivFunOnFintype_symm_single

added theorem Dfinsupp.equivProdDfinsupp_add

added theorem Dfinsupp.equivProdDfinsupp_smul

added def Dfinsupp.erase

added def Dfinsupp.eraseAddHom

added theorem Dfinsupp.erase_add

added theorem Dfinsupp.erase_add_single

added theorem Dfinsupp.erase_apply

added theorem Dfinsupp.erase_def

added theorem Dfinsupp.erase_eq_sub_single

added theorem Dfinsupp.erase_ne

added theorem Dfinsupp.erase_neg

added theorem Dfinsupp.erase_same

added theorem Dfinsupp.erase_single

added theorem Dfinsupp.erase_single_ne

added theorem Dfinsupp.erase_single_same

added theorem Dfinsupp.erase_sub

added theorem Dfinsupp.erase_zero

added def Dfinsupp.evalAddMonoidHom

added theorem Dfinsupp.ext

added theorem Dfinsupp.ext_iff

added def Dfinsupp.extendWith

added theorem Dfinsupp.extendWith_none

added theorem Dfinsupp.extendWith_single_zero

added theorem Dfinsupp.extendWith_some

added theorem Dfinsupp.extendWith_zero

added def Dfinsupp.filter

added def Dfinsupp.filterAddMonoidHom

added def Dfinsupp.filterLinearMap

added theorem Dfinsupp.filter_add

added theorem Dfinsupp.filter_apply

added theorem Dfinsupp.filter_apply_neg

added theorem Dfinsupp.filter_apply_pos

added theorem Dfinsupp.filter_def

added theorem Dfinsupp.filter_ne_eq_erase'

added theorem Dfinsupp.filter_ne_eq_erase

added theorem Dfinsupp.filter_neg

added theorem Dfinsupp.filter_pos_add_filter_neg

added theorem Dfinsupp.filter_single

added theorem Dfinsupp.filter_single_neg

added theorem Dfinsupp.filter_single_pos

added theorem Dfinsupp.filter_smul

added theorem Dfinsupp.filter_sub

added theorem Dfinsupp.filter_zero

added theorem Dfinsupp.finite_support

added theorem Dfinsupp.finset_sum_apply

added theorem Dfinsupp.induction₂

added theorem Dfinsupp.infinite_of_exists_right

added def Dfinsupp.liftAddHom

added theorem Dfinsupp.liftAddHom_apply_single

added theorem Dfinsupp.liftAddHom_comp_single

added theorem Dfinsupp.liftAddHom_singleAddHom

added def Dfinsupp.mapRange.addEquiv

added theorem Dfinsupp.mapRange.addEquiv_refl

added theorem Dfinsupp.mapRange.addEquiv_symm

added theorem Dfinsupp.mapRange.addEquiv_trans

added def Dfinsupp.mapRange.addMonoidHom

added theorem Dfinsupp.mapRange.addMonoidHom_comp

added theorem Dfinsupp.mapRange.addMonoidHom_id

added def Dfinsupp.mapRange

added theorem Dfinsupp.mapRange_add

added theorem Dfinsupp.mapRange_apply

added theorem Dfinsupp.mapRange_comp

added theorem Dfinsupp.mapRange_def

added theorem Dfinsupp.mapRange_id

added theorem Dfinsupp.mapRange_single

added theorem Dfinsupp.mapRange_zero

added theorem Dfinsupp.mem_support_iff

added theorem Dfinsupp.mem_support_toFun

added def Dfinsupp.mk

added def Dfinsupp.mkAddGroupHom

added theorem Dfinsupp.mk_add

added theorem Dfinsupp.mk_apply

added theorem Dfinsupp.mk_injective

added theorem Dfinsupp.mk_neg

added theorem Dfinsupp.mk_of_mem

added theorem Dfinsupp.mk_of_not_mem

added theorem Dfinsupp.mk_smul

added theorem Dfinsupp.mk_sub

added theorem Dfinsupp.mk_zero

added theorem Dfinsupp.neg_apply

added theorem Dfinsupp.not_mem_support_iff

added theorem Dfinsupp.nsmul_apply

added def Dfinsupp.piecewise

added theorem Dfinsupp.piecewise_apply

added theorem Dfinsupp.piecewise_single_erase

added def Dfinsupp.prod

added theorem Dfinsupp.prod_add_index

added theorem Dfinsupp.prod_comm

added theorem Dfinsupp.prod_eq_one

added theorem Dfinsupp.prod_eq_prod_fintype

added theorem Dfinsupp.prod_finset_sum_index

added theorem Dfinsupp.prod_inv

added theorem Dfinsupp.prod_mapRange_index

added theorem Dfinsupp.prod_mul

added theorem Dfinsupp.prod_neg_index

added theorem Dfinsupp.prod_one

added theorem Dfinsupp.prod_single_index

added theorem Dfinsupp.prod_subtypeDomain_index

added theorem Dfinsupp.prod_sum_index

added theorem Dfinsupp.prod_zero_index

added theorem Dfinsupp.sigmaCurry_add

added theorem Dfinsupp.sigmaCurry_apply

added theorem Dfinsupp.sigmaCurry_single

added theorem Dfinsupp.sigmaCurry_smul

added theorem Dfinsupp.sigmaCurry_zero

added theorem Dfinsupp.sigmaUncurry_add

added theorem Dfinsupp.sigmaUncurry_apply

added theorem Dfinsupp.sigmaUncurry_single

added theorem Dfinsupp.sigmaUncurry_smul

added theorem Dfinsupp.sigmaUncurry_zero

added def Dfinsupp.single

added def Dfinsupp.singleAddHom

added theorem Dfinsupp.single_add

added theorem Dfinsupp.single_add_erase

added theorem Dfinsupp.single_apply

added theorem Dfinsupp.single_eq_of_ne

added theorem Dfinsupp.single_eq_of_sigma_eq

added theorem Dfinsupp.single_eq_pi_single

added theorem Dfinsupp.single_eq_same

added theorem Dfinsupp.single_eq_single_iff

added theorem Dfinsupp.single_eq_zero

added theorem Dfinsupp.single_injective

added theorem Dfinsupp.single_left_injective

added theorem Dfinsupp.single_neg

added theorem Dfinsupp.single_smul

added theorem Dfinsupp.single_sub

added theorem Dfinsupp.single_zero

added theorem Dfinsupp.smul_apply

added theorem Dfinsupp.smul_sum

added theorem Dfinsupp.sub_apply

added def Dfinsupp.subtypeDomain

added def Dfinsupp.subtypeDomainAddMonoidHom

added def Dfinsupp.subtypeDomainLinearMap

added theorem Dfinsupp.subtypeDomain_add

added theorem Dfinsupp.subtypeDomain_apply

added theorem Dfinsupp.subtypeDomain_def

added theorem Dfinsupp.subtypeDomain_finsupp_sum

added theorem Dfinsupp.subtypeDomain_neg

added theorem Dfinsupp.subtypeDomain_smul

added theorem Dfinsupp.subtypeDomain_sub

added theorem Dfinsupp.subtypeDomain_sum

added theorem Dfinsupp.subtypeDomain_zero

added def Dfinsupp.sumAddHom

added theorem Dfinsupp.sumAddHom_add

added theorem Dfinsupp.sumAddHom_apply

added theorem Dfinsupp.sumAddHom_comm

added theorem Dfinsupp.sumAddHom_comp_single

added theorem Dfinsupp.sumAddHom_single

added theorem Dfinsupp.sumAddHom_singleAddHom

added theorem Dfinsupp.sumAddHom_zero

added theorem Dfinsupp.sum_apply

added theorem Dfinsupp.sum_single

added theorem Dfinsupp.sum_sub_index

added def Dfinsupp.support

added theorem Dfinsupp.support_add

added theorem Dfinsupp.support_eq_empty

added theorem Dfinsupp.support_erase

added theorem Dfinsupp.support_filter

added theorem Dfinsupp.support_mapRange

added theorem Dfinsupp.support_mk'_subset

added theorem Dfinsupp.support_mk_subset

added theorem Dfinsupp.support_neg

added theorem Dfinsupp.support_single_ne_zero

added theorem Dfinsupp.support_single_subset

added theorem Dfinsupp.support_smul

added theorem Dfinsupp.support_subset_iff

added theorem Dfinsupp.support_subtypeDomain

added theorem Dfinsupp.support_sum

added theorem Dfinsupp.support_update

added theorem Dfinsupp.support_update_ne_zero

added theorem Dfinsupp.support_zero

added theorem Dfinsupp.support_zipWith

added theorem Dfinsupp.toFun_eq_coe

added def Dfinsupp.update

added theorem Dfinsupp.update_eq_erase

added theorem Dfinsupp.update_eq_erase_add_single

added theorem Dfinsupp.update_eq_single_add_erase

added theorem Dfinsupp.update_eq_sub_add_single

added theorem Dfinsupp.update_self

added theorem Dfinsupp.zero_apply

added def Dfinsupp.zipWith

added theorem Dfinsupp.zipWith_apply

added theorem Dfinsupp.zipWith_def

added theorem Dfinsupp.zsmul_apply

added structure Dfinsupp

added theorem MonoidHom.coe_dfinsupp_prod

added theorem MonoidHom.dfinsupp_prod_apply

added theorem MonoidHom.map_dfinsupp_prod

added theorem MulEquiv.map_dfinsupp_prod

added theorem RingHom.map_dfinsupp_prod

added theorem RingHom.map_dfinsupp_sum

added theorem RingHom.map_dfinsupp_sumAddHom

added theorem dfinsupp_prod_mem

added theorem dfinsupp_sumAddHom_mem