Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-08 15:06 3ca4c270

View on Github →

chore(algebra/ordered_ring): use le instead of ge (#2986)

Estimated changes

Modified src/algebra/ordered_ring.lean

modified theorem le_of_mul_le_mul_left

modified theorem le_of_mul_le_mul_right

deleted theorem le_of_mul_le_of_ge_one

added theorem le_of_mul_le_of_one_le

modified theorem lt_of_mul_lt_mul_left

modified theorem lt_of_mul_lt_mul_right

modified theorem mul_lt_mul'

modified theorem mul_neg_of_neg_of_pos

modified theorem mul_neg_of_pos_of_neg

modified theorem mul_nonpos_of_nonneg_of_nonpos

modified theorem mul_nonpos_of_nonpos_of_nonneg

added theorem neg_one_lt_zero

modified theorem nonneg_le_nonneg_of_squares_le

added theorem one_le_two

modified theorem one_lt_two

deleted theorem two_ge_one

deleted theorem two_gt_one

deleted theorem zero_gt_neg_one