Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-04-13 19:25 56052335

View on Github →

feat(algebra/big_operators): add prod_sum (equating the product over a sum to the sum of all combinations)

Estimated changes

added theorem finset.prod_sum
added theorem finset.attach_empty
added theorem finset.attach_insert
added def finset.pi.cons
added theorem finset.pi.cons_ne
added theorem finset.pi.cons_same
added def finset.pi.empty
added theorem finset.pi_empty
added theorem finset.pi_insert
added theorem multiset.map_id
added theorem multiset.map_singleton
added theorem multiset.nodup_bind
added theorem multiset.nodup_pi
added theorem multiset.pmap_cons
added theorem multiset.pmap_zero
added theorem multiset.prod_bind