mathlib

eeb4bb66 - feat(algebra/big_operators): absolute values and big operators (#9027)

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