PR #1598 feat(algebra/big_operators): sum_ite

feat(algebra/big_operators): sum_ite #1598

mergify merged 3 commits into master from ChrisHughes24-patch-2

feat(algebra/big_operators): sum_ite

9970c9be

jcommelin commented on 2019-10-23

Update src/algebra/big_operators.lean

f9a8ad21

rwbarton approved these changes on 2019-10-23

rwbarton added ready-to-merge

Merge branch 'master' into ChrisHughes24-patch-2

5dc8c395

mergify merged b433afa7 into master 6 years ago

mergify deleted the ChrisHughes24-patch-2 branch 6 years ago

Reviewers

rwbarton

jcommelin

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone