Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-08-05 09:15 fc56c852

View on Github →

feat(algebra/order_functions): abs_nonpos_iff (#1299)

  • feat(algebra/ordered_group): abs_nonpos_iff
  • Update ordered_group.lean
  • move to order_functions

Estimated changes