mathlib3

adb763be - feat(algebra/big_operators): absolute values and big operators

feat(algebra/big_operators): absolute values and big operators This PR extends `absolute_value.add_le` and `absolute_value.map_mul` to `finset.sum` and `finset.prod` respectively.