Commit 2022-05-12 20:54 17102ae8
View on Github →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
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