mathlib3

2541387e - refactor(data/list/big_operators): review API (#12782)

refactor(data/list/big_operators): review API (#12782) * merge `prod_monoid` into `big_operators`; * review typeclass assumptions in some lemmas; * use `to_additive` in more lemmas.