Commit 2023-01-27 13:32 c0e3c105

View on Github →

feat: port Data.Finsupp.Defs (#1807)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Finsupp/Defs.lean

added theorem Finsupp.addHom_ext'

added theorem Finsupp.addHom_ext

added theorem Finsupp.add_apply

added theorem Finsupp.add_closure_setOf_eq_single

added def Finsupp.applyAddHom

added theorem Finsupp.card_support_eq_one'

added theorem Finsupp.card_support_eq_one

added theorem Finsupp.card_support_eq_zero

added theorem Finsupp.card_support_le_one'

added theorem Finsupp.card_support_le_one

added theorem Finsupp.coeFn_inj

added theorem Finsupp.coeFn_injective

added theorem Finsupp.coe_add

added theorem Finsupp.coe_eq_zero

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 def Finsupp.embDomain.addMonoidHom

added def Finsupp.embDomain

added theorem Finsupp.embDomain_add

added theorem Finsupp.embDomain_apply

added theorem Finsupp.embDomain_eq_zero

added theorem Finsupp.embDomain_inj

added theorem Finsupp.embDomain_injective

added theorem Finsupp.embDomain_mapRange

added theorem Finsupp.embDomain_notin_range

added theorem Finsupp.embDomain_single

added theorem Finsupp.embDomain_zero

added theorem Finsupp.eq_single_iff

added def Finsupp.equivFunOnFinite

added theorem Finsupp.equivFunOnFinite_single

added theorem Finsupp.equivFunOnFinite_symm_coe

added theorem Finsupp.equivFunOnFinite_symm_single

added def Finsupp.erase

added def Finsupp.eraseAddHom

added theorem Finsupp.erase_add

added theorem Finsupp.erase_add_single

added theorem Finsupp.erase_eq_sub_single

added theorem Finsupp.erase_ne

added theorem Finsupp.erase_of_not_mem_support

added theorem Finsupp.erase_same

added theorem Finsupp.erase_single

added theorem Finsupp.erase_single_ne

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_linear

added theorem Finsupp.induction₂

added def Finsupp.mapRange

added theorem Finsupp.mapRange_add'

added theorem Finsupp.mapRange_add

added theorem Finsupp.mapRange_apply

added theorem Finsupp.mapRange_comp

added theorem Finsupp.mapRange_id

added theorem Finsupp.mapRange_neg'

added theorem Finsupp.mapRange_neg

added theorem Finsupp.mapRange_single

added theorem Finsupp.mapRange_sub'

added theorem Finsupp.mapRange_sub

added theorem Finsupp.mapRange_zero

added theorem Finsupp.mem_support_iff

added theorem Finsupp.mem_support_onFinset

added theorem Finsupp.mem_support_single

added theorem Finsupp.mulHom_ext'

added theorem Finsupp.mulHom_ext

added theorem Finsupp.neg_apply

added theorem Finsupp.nonzero_iff_exists

added theorem Finsupp.not_mem_support_iff

added theorem Finsupp.ofSupportFinite_coe

added def Finsupp.onFinset

added theorem Finsupp.onFinset_apply

added theorem Finsupp.range_single_subset

added def Finsupp.single

added def Finsupp.singleAddHom

added theorem Finsupp.single_add

added theorem Finsupp.single_add_erase

added theorem Finsupp.single_add_single_eq_single_add_single

added theorem Finsupp.single_apply

added theorem Finsupp.single_apply_eq_zero

added theorem Finsupp.single_apply_left

added theorem Finsupp.single_apply_mem

added theorem Finsupp.single_apply_ne_zero

added theorem Finsupp.single_eq_indicator

added theorem Finsupp.single_eq_of_ne

added theorem Finsupp.single_eq_pi_single

added theorem Finsupp.single_eq_same

added theorem Finsupp.single_eq_single_iff

added theorem Finsupp.single_eq_update

added theorem Finsupp.single_eq_zero

added theorem Finsupp.single_injective

added theorem Finsupp.single_left_inj

added theorem Finsupp.single_left_injective

added theorem Finsupp.single_of_embDomain_single

added theorem Finsupp.single_of_single_apply

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_embDomain

added theorem Finsupp.support_eq_empty

added theorem Finsupp.support_eq_singleton'

added theorem Finsupp.support_eq_singleton

added theorem Finsupp.support_erase

added theorem Finsupp.support_mapRange

added theorem Finsupp.support_mapRange_of_injective

added theorem Finsupp.support_neg

added theorem Finsupp.support_nonempty_iff

added theorem Finsupp.support_onFinset

added theorem Finsupp.support_onFinset_subset

added theorem Finsupp.support_single_disjoint

added theorem Finsupp.support_single_ne_bot

added theorem Finsupp.support_single_ne_zero

added theorem Finsupp.support_single_subset

added theorem Finsupp.support_sub

added theorem Finsupp.support_subset_iff

added theorem Finsupp.support_subset_singleton'

added theorem Finsupp.support_subset_singleton

added theorem Finsupp.support_update

added theorem Finsupp.support_update_ne_zero

added theorem Finsupp.support_update_zero

added theorem Finsupp.support_zero

added theorem Finsupp.support_zipWith

added theorem Finsupp.unique_ext

added theorem Finsupp.unique_ext_iff

added theorem Finsupp.unique_single

added theorem Finsupp.unique_single_eq_iff

added def Finsupp.update

added theorem Finsupp.update_eq_erase_add_single

added theorem Finsupp.update_eq_single_add_erase

added theorem Finsupp.update_eq_sub_add_single

added theorem Finsupp.update_self

added theorem Finsupp.zero_apply

added theorem Finsupp.zero_update

added def Finsupp.zipWith

added theorem Finsupp.zipWith_apply

added structure Finsupp