mathlib
b433afa7 - feat(algebra/big_operators): sum_ite (#1598)

Commit
6 years ago
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>
Author
Committer
Parents
Loading