mathlib3

17102ae8 - feat(algebra/big_operators/basic): add `sum_erase_lt_of_pos` (#14066)

feat(algebra/big_operators/basic): add `sum_erase_lt_of_pos` (#14066) `sum_erase_lt_of_pos (hd : d ∈ s) (hdf : 0 < f d) : ∑ (m : ℕ) in s.erase d, f m < ∑ (m : ℕ) in s, f m`