Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-12-07 17:24 f09abb1c

View on Github →

feat(data/finsupp): add type of functions with finite support

Estimated changes

Created data/finsupp.lean

added theorem finsupp.add_apply

added def finsupp.comap_domain

added theorem finsupp.comap_domain_add

added theorem finsupp.comap_domain_apply

added theorem finsupp.comap_domain_finsupp_sum

added theorem finsupp.comap_domain_neg

added theorem finsupp.comap_domain_sub

added theorem finsupp.comap_domain_sum

added theorem finsupp.comap_domain_zero

added theorem finsupp.ext

added theorem finsupp.finite_supp

added def finsupp.map_domain

added theorem finsupp.map_domain_add

added theorem finsupp.map_domain_comp

added theorem finsupp.map_domain_congr

added theorem finsupp.map_domain_finset_sum

added theorem finsupp.map_domain_id

added theorem finsupp.map_domain_single

added theorem finsupp.map_domain_sum

added theorem finsupp.map_domain_support

added theorem finsupp.map_domain_zero

added def finsupp.map_range

added theorem finsupp.map_range_apply

added theorem finsupp.mem_support_iff

added theorem finsupp.mul_def

added theorem finsupp.neg_apply

added theorem finsupp.one_def

added theorem finsupp.prod_single

added def finsupp.single

added theorem finsupp.single_add

added theorem finsupp.single_apply

added theorem finsupp.single_eq_of_ne

added theorem finsupp.single_eq_same

added theorem finsupp.single_mul_single

added theorem finsupp.single_zero

added theorem finsupp.sub_apply

added def finsupp.subtype_domain

added theorem finsupp.subtype_domain_add

added theorem finsupp.subtype_domain_apply

added theorem finsupp.subtype_domain_finsupp_sum

added theorem finsupp.subtype_domain_neg

added theorem finsupp.subtype_domain_sub

added theorem finsupp.subtype_domain_sum

added theorem finsupp.subtype_domain_zero

added def finsupp.sum

added theorem finsupp.sum_add

added theorem finsupp.sum_add_index

added theorem finsupp.sum_apply

added theorem finsupp.sum_comap_domain_index

added theorem finsupp.sum_finset_sum_index

added theorem finsupp.sum_map_domain_index

added theorem finsupp.sum_map_range_index

added theorem finsupp.sum_neg

added theorem finsupp.sum_neg_index

added theorem finsupp.sum_single

added theorem finsupp.sum_single_index

added theorem finsupp.sum_sub_index

added theorem finsupp.sum_subtype_domain_index

added theorem finsupp.sum_sum_index

added theorem finsupp.sum_zero

added theorem finsupp.sum_zero_index

added def finsupp.support

added theorem finsupp.support_add

added theorem finsupp.support_map_range

added theorem finsupp.support_single_ne_zero

added theorem finsupp.support_single_subset

added theorem finsupp.support_sum

added theorem finsupp.support_zero

added theorem finsupp.support_zip_with

added def finsupp.to_comm_ring

added def finsupp.to_comm_semiring

added def finsupp.to_ring

added def finsupp.to_semiring

added theorem finsupp.zero_apply

added def finsupp.zip_with

added theorem finsupp.zip_with_apply

added def finsupp