big_operators): add `list.prod_map_mul` (#12029)

Commit

3 years ago

feat(data/list/big_operators): add `list.prod_map_mul` (#12029) This is an analogue of the corresponding lemma `multiset.prod_map_mul`.

Author

kmill

Parents