mathlib3

80c7ac1c - feat(algebra/big_operators/order): add fintype.sum_mono and fintype.sum_strict_mono (#6040)