Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-06 09:03 55931556

View on Github →

feat(*): lemmas on sums and products over fintypes (#2598)

Estimated changes

Modified src/data/finsupp.lean

added theorem finsupp.prod_pow

Modified src/data/fintype/card.lean

added theorem finset.prod_fiberwise

modified theorem fintype.card_eq_sum_ones

added theorem fintype.prod_congr

added theorem fintype.prod_eq_one

added theorem fintype.prod_fiberwise

added theorem fintype.prod_sum_type

added theorem fintype.prod_unique