mathlib3

feat(algebra/big_operators): missing lemmas

#2259

Merged