# Commit2021-05-15 16:28172195bb

View on Github →

feat(algebra/{ordered_monoid, ordered_monoid_lemmas}): split the `ordered_[...]` typeclasses (#7371) This PR tries to split the ordering assumptions from the algebraic assumptions on the operations in the `ordered_[...]` hierarchy. The strategy is to introduce two more flexible typeclasses, `covariant_class` and `contravariant_class`.

• `covariant_class` models the implication `a ≤ b → c * a ≤ c * b` (multiplication is monotone),
• `contravariant_class` models the implication `a * b < a * c → b < c`. Since `co(ntra)variant_class` takes as input the operation (typically `(+)` or `(*)`) and the order relation (typically `(≤)` or `(<)`), these are the only two typeclasses that I have used. The general approach is to formulate the lemma that you are interested in and prove it, with the `ordered_[...]` typeclass of your liking. After that, you convert the single typeclass, say `[ordered_cancel_monoid M]`, to three typeclasses, e.g. `[partial_order M] [left_cancel_semigroup M] [covariant_class M M (function.swap (*)) (≤)]` and have a go at seeing if the proof still works! Note that it is possible (or even expected) to combine several `co(ntra)variant_class` assumptions together. Indeed, the usual `ordered` typeclasses arise from assuming the pair `[covariant_class M M (*) (≤)] [contravariant_class M M (*) (<)]` on top of order/algebraic assumptions. A formal remark is that normally `covariant_class` uses the `(≤)`-relation, while `contravariant_class` uses the `(<)`-relation. This need not be the case in general, but seems to be the most common usage. In the opposite direction, the implication `[semigroup α] [partial_order α] [contravariant_class α α (*) (≤)] => left_cancel_semigroup α` holds (note the `co*ntra*` assumption and the `(≤)`-relation). Zulip: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/ordered.20stuff

#### Estimated changes

deleted theorem le_mul_iff_one_le_left'
deleted theorem le_mul_iff_one_le_right'
deleted theorem le_mul_of_le_mul_left
deleted theorem le_mul_of_le_mul_right
deleted theorem le_mul_of_le_of_one_le
deleted theorem le_mul_of_one_le_left'
deleted theorem le_mul_of_one_le_of_le
deleted theorem le_mul_of_one_le_right'
deleted theorem le_of_mul_le_mul_left'
deleted theorem le_of_mul_le_mul_right'
deleted theorem lt_mul_iff_one_lt_left'
deleted theorem lt_mul_iff_one_lt_right'
deleted theorem lt_mul_of_le_of_one_lt
deleted theorem lt_mul_of_lt_mul_left
deleted theorem lt_mul_of_lt_mul_right
deleted theorem lt_mul_of_lt_of_one_le'
deleted theorem lt_mul_of_lt_of_one_le
deleted theorem lt_mul_of_lt_of_one_lt'
deleted theorem lt_mul_of_lt_of_one_lt
deleted theorem lt_mul_of_one_le_of_lt'
deleted theorem lt_mul_of_one_le_of_lt
deleted theorem lt_mul_of_one_lt_left'
deleted theorem lt_mul_of_one_lt_of_le
deleted theorem lt_mul_of_one_lt_of_lt'
deleted theorem lt_mul_of_one_lt_of_lt
deleted theorem lt_mul_of_one_lt_right'
deleted theorem lt_of_mul_lt_mul_left'
deleted theorem lt_of_mul_lt_mul_right'
deleted theorem monotone.const_mul'
deleted theorem monotone.mul'
deleted theorem monotone.mul_const'
deleted theorem mul_eq_one_iff'
deleted theorem mul_le_iff_le_one_left'
deleted theorem mul_le_iff_le_one_right'
deleted theorem mul_le_mul'
deleted theorem mul_le_mul_iff_left
deleted theorem mul_le_mul_iff_right
deleted theorem mul_le_mul_left'
deleted theorem mul_le_mul_right'
deleted theorem mul_le_mul_three
deleted theorem mul_le_of_le_of_le_one'
deleted theorem mul_le_of_le_of_le_one
deleted theorem mul_le_of_le_one_left'
deleted theorem mul_le_of_le_one_of_le'
deleted theorem mul_le_of_le_one_of_le
deleted theorem mul_le_of_le_one_right'
deleted theorem mul_le_of_mul_le_left
deleted theorem mul_le_of_mul_le_right
deleted theorem mul_le_one'
deleted theorem mul_lt_iff_lt_one_left'
deleted theorem mul_lt_iff_lt_one_right'
deleted theorem mul_lt_mul'''
deleted theorem mul_lt_mul_iff_left
deleted theorem mul_lt_mul_iff_right
deleted theorem mul_lt_mul_left'
deleted theorem mul_lt_mul_of_le_of_lt
deleted theorem mul_lt_mul_of_lt_of_le
deleted theorem mul_lt_mul_right'
deleted theorem mul_lt_of_le_of_lt_one
deleted theorem mul_lt_of_le_one_of_lt'
deleted theorem mul_lt_of_le_one_of_lt
deleted theorem mul_lt_of_lt_of_le_one'
deleted theorem mul_lt_of_lt_of_le_one
deleted theorem mul_lt_of_lt_of_lt_one'
deleted theorem mul_lt_of_lt_of_lt_one
deleted theorem mul_lt_of_lt_one_of_le
deleted theorem mul_lt_of_lt_one_of_lt'
deleted theorem mul_lt_of_lt_one_of_lt
deleted theorem mul_lt_of_mul_lt_left
deleted theorem mul_lt_of_mul_lt_right
deleted theorem mul_lt_one'
deleted theorem mul_lt_one
deleted theorem one_le_mul
deleted theorem one_lt_mul'
deleted theorem one_lt_mul_of_le_of_lt'
deleted theorem one_lt_mul_of_lt_of_le'
deleted theorem pos_of_gt
modified theorem with_zero.mul_le_mul_left
modified theorem with_zero.zero_lt_coe