Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-02-20 15:36 140c6728

View on Github →

feat(algebra/order_functions): add abs_le_max_abs_abs; and relations between mul and max / min (suggested by @PatrickMassot)

Estimated changes