mathlib3

4767b303 - feat(algebra/big_operators): more general prod_insert_one (#3426)

feat(algebra/big_operators): more general prod_insert_one (#3426) I found I had a use for a slightly more general version of `prod_insert_one` / `sum_insert_zero`. Add that version and use it in the proof of `prod_insert_one`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>