Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-24 12:36 9b759111

View on Github →

feat(algebra/order): lemmas about cmp and arithmetic operations (#16207)

Estimated changes

added theorem cmp_div_one'
added theorem cmp_mul_left'
added theorem cmp_mul_right'
added theorem cmp_mul_neg_left
added theorem cmp_mul_neg_right
added theorem cmp_mul_pos_left
added theorem cmp_mul_pos_right