Theorem finset.abs_sum_le_sum_abs
Modification history
2021-04-15 15:46
src/algebra/big_operators/order.lean
refactor(algebra/big_operators/order): use `to_additive` (#7173) …
Modified finset.abs_sum_le_sum_absView on Github →2020-10-27 11:55
src/algebra/big_operators/order.lean
refactor(*): drop `decidable_linear_order`, switch to Lean 3.22.0 (#4762) …
Modified finset.abs_sum_le_sum_absView on Github →2020-07-22 10:18
src/algebra/big_operators/basic.lean
refactor(algebra/big_operators): split file, reduce imports (#3495) …
Modified finset.abs_sum_le_sum_absView on Github →2019-03-26 18:22
src/algebra/big_operators.lean
feat(data/multiset,data/finset): add multiset./finset.le_sum_of_additive
Modified finset.abs_sum_le_sum_absView on Github →2017-09-21 13:22
algebra/big_operators.lean
feat(topology/lebesgue_measure): add Lebesgue outer measure; show that the lower half open interval is measurable
Added finset.abs_sum_le_sum_absView on Github →