Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-18 07:06 04948074

View on Github →

feat(algebra/ordered_*): cleanup and projection notation (#3850) Also add a few new projection notations.

Estimated changes

Modified src/algebra/order.lean

Modified src/algebra/ordered_field.lean

Modified src/algebra/ordered_group.lean

modified theorem mul_le_mul_three

modified theorem with_top.zero_lt_coe

Modified src/algebra/ordered_ring.lean

modified theorem canonically_ordered_semiring.mul_le_mul

modified theorem canonically_ordered_semiring.zero_lt_one

modified theorem mul_lt_mul

modified theorem one_le_two

deleted theorem ordered_semiring.mul_le_mul_of_nonneg_left

deleted theorem ordered_semiring.mul_le_mul_of_nonneg_right