feat(algebra/big_operators): some big operator lemmas (#13066)
Note that `prod_coe_sort` is essentially `prod_finset_coe` restated with the relatively new `finset.has_coe_to_sort`. I can also place `prod_finset_coe` with `prod_coe_sort` if we prefer.
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
