Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-23 20:48 b433afa7

View on Github →

feat(algebra/big_operators): sum_ite (#1598)

  • feat(algebra/big_operators): sum_ite rename the current sum_ite to sum_ite_eq and add a more general version
  • Update src/algebra/big_operators.lean Co-Authored-By: Johan Commelin johan@commelin.net

Estimated changes

modified theorem finset.prod_ite
added theorem finset.prod_ite_eq