Commit 2021-07-14 08:37 8e5af430

chore(algebra/big_operators/basic): rename sum_(nat/int)_cast and (nat/int).coe_prod (#8264) The current names aren't great because

1. For sum_nat_cast and sum_int_cast, the LHS isn't a sum of casts but a cast of sums, and it doesn't follow any other naming convention (nat.cast_... or ....coe_sum).
2. For .coe_prod, the coercion from ℕ or ℤ should be called cast.