Mathlib v3 is deprecated. Go to Mathlib v4

Theorem multiset.abs_sum_le_sum_abs

Modification history

2021-12-25 19:14
src/algebra/big_operators/multiset.lean
split(algebra/big_operators/multiset): Split off `data.multiset.basic` (#11043) …
Modified multiset.abs_sum_le_sum_absView on Github →
2021-08-23 10:17
src/algebra/big_operators/basic.lean
chore(data/multiset/basic): move abs_sum_le_sum_abs from algebra/big_operators/basic.lean. (#8804) …
Modified multiset.abs_sum_le_sum_absView on Github →
2021-06-04 03:56
src/algebra/big_operators/basic.lean
chore(data/finset|multiset|finsupp): reduce algebra/ imports (#7797)
Modified multiset.abs_sum_le_sum_absView on Github →
2020-10-27 11:55
src/data/multiset/basic.lean
refactor(*): drop `decidable_linear_order`, switch to Lean 3.22.0 (#4762) …
Modified multiset.abs_sum_le_sum_absView on Github →
2019-03-26 18:22
src/data/multiset.lean
feat(data/multiset,data/finset): add multiset./finset.le_sum_of_additive
Added multiset.abs_sum_le_sum_absView on Github →