Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes