Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-03 20:51 e593ffa6

View on Github →

feat(algebra/ordered*): more simp lemmas (#4359) Simplify expressions like 0 < a * b, 0 < a / b, a / b < 1 etc. to FOL formulas of inequalities on a, b.

Estimated changes

modified theorem pow_nonneg
modified theorem pow_pos
added theorem inv_eq_one'
added theorem ne.le_iff_lt
added theorem ne.lt_or_lt
added theorem div_le_one_iff
added theorem div_lt_one_iff
added theorem div_neg_iff
added theorem div_nonneg_iff
added theorem div_nonpos_iff
added theorem div_pos_iff
added theorem inv_le_one_iff
added theorem inv_lt_one_iff
added theorem inv_lt_one_iff_of_pos
added theorem one_le_div_iff
added theorem one_le_inv_iff
added theorem one_lt_div_iff
added theorem one_lt_inv_iff
added theorem mul_neg_iff
added theorem mul_nonneg_iff
added theorem mul_nonpos_iff
added theorem mul_pos_iff
modified theorem pos_of_mul_pos_left
modified theorem pos_of_mul_pos_right
modified theorem int.coe_nat_nonneg