mathlib

d43daf01 - feat(algebra/big_operators/order): add unbundled is_absolute_value.sum_le and map_prod (#10104)

feat(algebra/big_operators/order): add unbundled is_absolute_value.sum_le and map_prod (#10104) Add unbundled versions of two existing lemmas. Additionally generalize a few typeclass assumptions in an earlier file. From the flt-regular project