Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-24 08:39 5344da4c

View on Github →

feat(algebra/big_operators): simp lemmas (#1471)

feat(algebra/big_operators): simp lemmas
remove @[simp]

Estimated changes

Modified src/algebra/big_operators.lean

added theorem finset.prod_ite

added theorem finset.sum_boole_mul

added theorem finset.sum_mul_boole

Modified src/data/finset.lean

added theorem finset.filter_eq