Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-08-12 10:14 01cb33cb

View on Github →

feat(algebra/ordered_ring): pos_of_mul_neg_left and similar (#1313)

Estimated changes

Modified src/algebra/ordered_ring.lean

added theorem neg_of_mul_pos_left

added theorem neg_of_mul_pos_right

added theorem nonneg_of_mul_nonpos_left

added theorem nonneg_of_mul_nonpos_right

added theorem nonpos_of_mul_nonneg_left

added theorem nonpos_of_mul_nonneg_right

added theorem pos_of_mul_neg_left

added theorem pos_of_mul_neg_right