Commit 2022-12-12 09:20 b02da0a1

View on Github →

feat: port Algebra.Order.WithZero (#903) mathlib3 655994e298904d7e5bbd1e18c95defd7b543eb94 All remaining issues are elaboration problems involving the order-dual. I think these should be debugged carefully, but I am not sure whether I will have time this weekend, so help is welcome. I fixed these with a bunch of @ and opened a Zulip thread.

Estimated changes

added theorem Units.zero_lt
added theorem div_le_div_left₀
added theorem div_le_div_right₀
added theorem div_le_div₀
added theorem div_le_iff₀
added theorem inv_le_inv₀
added theorem inv_le_one₀
added theorem inv_lt_inv₀
added theorem le_div_iff₀
added theorem le_mul_inv_iff₀
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_iff₀
added theorem mul_inv_le_of_le_mul
added theorem mul_le_mul_left₀
added theorem mul_le_mul_right₀
added theorem mul_le_one₀
added theorem mul_lt_mul₀
added theorem mul_lt_right₀
added theorem ne_zero_of_lt
added theorem not_lt_zero'
added theorem one_le_inv₀
added theorem one_le_mul₀
added theorem zero_le'
added theorem zero_lt_iff