Mathlib v3 is deprecated. Go to Mathlib v4

Theorem add_le_iff_nonpos_right

Modification history

2020-06-09 17:36
src/algebra/ordered_group.lean
refactor(algebra/ordered_group): multiplicative versions of ordered monoids/groups (#2844) …
Deleted add_le_iff_nonpos_rightView on Github →
2020-05-18 13:38
src/algebra/ordered_group.lean
refactor(algebra): merge init_.algebra into algebra (#2707) …
Modified add_le_iff_nonpos_rightView on Github →
2019-08-15 20:26
src/algebra/ordered_group.lean
feat(*): lemmas needed for two projects (#1294) …
Added add_le_iff_nonpos_rightView on Github →