Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-07 02:18 a1057a3b

View on Github →

feat(data/finsum): sums over sets and types with no finiteness hypotheses (#6355) This rather large PR is mostly work of Jason KY. It is all an API for finsum and finsum_in, sums over sets with no finiteness assumption, and which return zero if the sum is infinite.

Estimated changes

added theorem finprod_cond_eq_left
added theorem finprod_cond_eq_right
added theorem finprod_congr
added theorem finprod_congr_Prop
added theorem finprod_def
added theorem finprod_eq_dif
added theorem finprod_eq_if
added theorem finprod_eq_prod
added theorem finprod_false
added theorem finprod_mem_Union
added theorem finprod_mem_bUnion
added theorem finprod_mem_coe_finset
added theorem finprod_mem_comm
added theorem finprod_mem_congr
added theorem finprod_mem_def
added theorem finprod_mem_empty
added theorem finprod_mem_eq_prod
added theorem finprod_mem_image'
added theorem finprod_mem_image
added theorem finprod_mem_induction
added theorem finprod_mem_insert'
added theorem finprod_mem_insert
added theorem finprod_mem_insert_one
added theorem finprod_mem_mul_diff'
added theorem finprod_mem_mul_diff
added theorem finprod_mem_one
added theorem finprod_mem_pair
added theorem finprod_mem_range'
added theorem finprod_mem_range
added theorem finprod_mem_sUnion
added theorem finprod_mem_singleton
added theorem finprod_mem_union''
added theorem finprod_mem_union'
added theorem finprod_mem_union
added theorem finprod_mem_univ
added theorem finprod_mul_distrib
added theorem finprod_of_empty
added theorem finprod_one
added theorem finprod_true
added theorem finprod_unique
added theorem monoid_hom.map_finprod
deleted theorem dfinsupp.finite_supp
modified theorem set.finite.coe_to_finset
added theorem set.finite.of_preimage