Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-11 02:45 89bff5e7

View on Github →

feat(algebra/big_operators): add product versions of some sum lemmas (#11358) and to_additive to get the old ones back

Estimated changes

Modified src/algebra/big_operators/multiset.lean

added theorem multiset.le_prod_of_mem

deleted theorem multiset.le_sum_of_mem

added theorem multiset.prod_eq_one_iff

deleted theorem multiset.sum_eq_zero_iff

Modified src/data/list/big_operators.lean

added theorem list.prod_eq_one_iff

deleted theorem list.sum_eq_zero_iff