Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nonneg_of_mul_nonpos_right

Modification history

2019-08-12 10:14
src/algebra/ordered_ring.lean
feat(algebra/ordered_ring): pos_of_mul_neg_left and similar (#1313)
Added nonneg_of_mul_nonpos_rightView on Github →