mathlib3

08aff2ca - feat(algebra/big_operators/basic): edit `finset.sum/prod_range_succ` (#6676)

feat(algebra/big_operators/basic): edit `finset.sum/prod_range_succ` (#6676) - Change the RHS of the statement of `sum_range_succ` from `f n + ∑ x in range n, f x` to `∑ x in range n, f x + f n` - Change the RHS of the statement of `prod_range_succ` from `f n * ∑ x in range n, f x` to `∑ x in range n, f x * f n` The old versions of those lemmas are now called `sum_range_succ_comm` and `prod_range_succ_comm`, respectively. See [this conversation](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/break.20off.20last.20term.20of.20summation/near/229634503) on Zulip. Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>