Commit 2023-01-30 08:00 62a7ce4f

View on Github →

feat: port Algebra.BigOperators.Finsupp (#1900) Some simpNF issues & some leaky classicals caused trouble. But done now!

Estimated changes

added theorem Finset.sum_apply'
added theorem Finsupp.coe_finset_sum
added theorem Finsupp.coe_sum
added theorem Finsupp.mul_prod_erase
added theorem Finsupp.mul_sum
added theorem Finsupp.onFinset_prod
added def Finsupp.prod
added theorem Finsupp.prod_add_index
added theorem Finsupp.prod_comm
added theorem Finsupp.prod_congr
added theorem Finsupp.prod_embDomain
added theorem Finsupp.prod_fintype
added theorem Finsupp.prod_inv
added theorem Finsupp.prod_ite_eq'
added theorem Finsupp.prod_ite_eq
added theorem Finsupp.prod_mul
added theorem Finsupp.prod_neg_index
added theorem Finsupp.prod_pow
added theorem Finsupp.prod_sum_index
added theorem Finsupp.single_sum
added theorem Finsupp.sum_apply'
added theorem Finsupp.sum_apply
added theorem Finsupp.sum_mul
added theorem Finsupp.sum_single
added theorem Finsupp.sum_sub
added theorem Finsupp.sum_sub_index
added theorem Finsupp.sum_sum_index'
added theorem Finsupp.sum_zero
added theorem Finsupp.support_sum
added theorem map_finsupp_prod