Commit 2021-08-23 10:17 a52a9fe3
View on Github →chore(data/multiset/basic): move abs_sum_le_sum_abs from algebra/big_operators/basic.lean. (#8804) There doesn't seem to be a reason for the place it has now.
chore(data/multiset/basic): move abs_sum_le_sum_abs from algebra/big_operators/basic.lean. (#8804) There doesn't seem to be a reason for the place it has now.