mathlib

8e5af430 - chore(algebra/big_operators/basic): rename sum_(nat/int)_cast and (nat/int).coe_prod (#8264)

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`.