Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-17 19:57 b5baf555

View on Github →

feat(algebra/linear_ordered_comm_group_with_zero) define linear_ordered_comm_group_with_zero (#3072)

Estimated changes

added theorem div_le_div'
added theorem inv_le_inv''
added theorem inv_lt_inv''
added theorem le_mul_inv_of_mul_le
added theorem le_of_le_mul_right
added theorem le_zero_iff
added theorem mul_inv_le_of_le_mul
added theorem mul_inv_lt_of_lt_mul'
added theorem mul_lt_mul''''
added theorem mul_lt_right'
added theorem ne_zero_of_lt
added theorem not_lt_zero'
added theorem zero_le'
added theorem zero_le_one'
added theorem zero_lt_iff
added theorem zero_lt_one'
added theorem zero_lt_unit
added theorem div_le_div_iff'