basic): Sum of `ite` (#16825)

Commit

3 years ago

feat(algebra/big_operators/basic): Sum of `ite` (#16825) A sum of if then else that don't happen simultaneously can be written as a single if then else.

Author

YaelDillies

Parents

138f1db8

mathlib d4f69d96 - feat(algebra/big_operators/basic): Sum of `ite` (#16825)

mathlib
d4f69d96 - feat(algebra/big_operators/basic): Sum of `ite` (#16825)