Commit 2021-04-07 19:05 08aff2ca

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 on Zulip.