Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-03-10 20:37 b1540929

View on Github →

feat(data/finsupp): make finsupp computable; add induction rule; removed comap_domain

Estimated changes

Modified data/finsupp.lean

added theorem finset.mem_subtype

modified theorem finsupp.add_apply

deleted def finsupp.comap_domain

deleted theorem finsupp.comap_domain_add

deleted theorem finsupp.comap_domain_apply

deleted theorem finsupp.comap_domain_finsupp_sum

deleted theorem finsupp.comap_domain_neg

deleted theorem finsupp.comap_domain_sub

deleted theorem finsupp.comap_domain_sum

deleted theorem finsupp.comap_domain_zero

added def finsupp.erase

added theorem finsupp.erase_ne

added theorem finsupp.erase_same

modified def finsupp.filter

modified theorem finsupp.filter_pos_add_filter_neg

modified theorem finsupp.finite_supp

modified theorem finsupp.map_domain_finset_sum

modified def finsupp.map_range

modified theorem finsupp.map_range_apply

modified theorem finsupp.mem_support_iff

added def finsupp.on_finset

added theorem finsupp.on_finset_apply

deleted theorem finsupp.prod_comap_domain_index

modified theorem finsupp.prod_finset_sum_index

modified theorem finsupp.prod_map_range_index

modified theorem finsupp.prod_neg_index

modified theorem finsupp.prod_single

modified theorem finsupp.prod_single_index

modified theorem finsupp.prod_sum_index

modified theorem finsupp.single_add

added theorem finsupp.single_add_erase

modified theorem finsupp.single_apply

modified theorem finsupp.single_eq_of_ne

modified theorem finsupp.single_eq_same

modified theorem finsupp.single_zero

modified def finsupp.subtype_domain

modified theorem finsupp.subtype_domain_zero

modified theorem finsupp.sum_apply

deleted def finsupp.support

modified theorem finsupp.support_add

added theorem finsupp.support_eq_empty

added theorem finsupp.support_erase

modified theorem finsupp.support_map_range

added theorem finsupp.support_on_finset_subset

modified theorem finsupp.support_single_ne_zero

modified theorem finsupp.support_single_subset

modified theorem finsupp.support_subset_iff

added theorem finsupp.support_subtype_domain

modified theorem finsupp.support_sum

modified theorem finsupp.support_zero

modified theorem finsupp.support_zip_with

modified def finsupp.zip_with

modified theorem finsupp.zip_with_apply

added structure finsupp

deleted def finsupp

Modified linear_algebra/basic.lean