Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-12-13 13:09 8369c7d8

View on Github →

feat(data/finsupp): big product over finsupp (big sum is now derived from it)

Estimated changes

Modified data/finsupp.lean

added def finsupp.prod

added theorem finsupp.prod_add_index

added theorem finsupp.prod_comap_domain_index

added theorem finsupp.prod_finset_sum_index

added theorem finsupp.prod_map_domain_index

added theorem finsupp.prod_map_range_index

added theorem finsupp.prod_neg_index

added theorem finsupp.prod_single_index

added theorem finsupp.prod_subtype_domain_index

added theorem finsupp.prod_sum_index

added theorem finsupp.prod_zero_index

deleted theorem finsupp.sum_add_index

deleted theorem finsupp.sum_comap_domain_index

deleted theorem finsupp.sum_finset_sum_index

deleted theorem finsupp.sum_map_domain_index

deleted theorem finsupp.sum_map_range_index

deleted theorem finsupp.sum_neg_index

deleted theorem finsupp.sum_single_index

deleted theorem finsupp.sum_subtype_domain_index

deleted theorem finsupp.sum_sum_index

deleted theorem finsupp.sum_zero_index