[Merged by Bors] - feat(algebra/order/monoid): Co/contravariant classes for with_bot/with_top

[YaelDillies]

Add the covariant_class (with_bot α) (with_bot α) (+) (≤) and contravariant_class (with_bot α) (with_bot α) (+) (<) instances, as well as the lemmas that covariant_class (with_bot α) (with_bot α) (+) (<) and contravariant_class (with_bot α) (with_bot α) (+) (≤) almost hold.

On the way, match the APIs for with_bot/with_top by adding missing lemmas.

Co-authored-by: Wrenna Robson wren.robson@gmail.com

---

Sorry, the diff is a bit mangled because I had to move with_top/with_bot down the file to use order_dual. Note that I am not adding with_top.add_lt_add on purpose. We are currently unsure what the correct typeclass assumptions and whether we are not requiring a new one.

[adomani]

I think that this looks very nice!

Why did you do the with_top/bot for has_add and not for @[to_additive] has_mul? Is it already available somewhere else? I'm thinking of nnreal/ennreal where it might be useful to get covariant assumptions for addition and multiplication at the same time.

[YaelDillies]

with_top and with_bot do not have multiplication by default. I believe this is because that would disagree with the one on ennreal as 0 * ∞ = ∞ * 0 = 0 (instead of 0 * ∞ = ∞ * 0 = ∞).

[adomani]

Ah, I see! Thanks for the explanation!

[adomani]

There starts being quite a bit of code-repetition floating around co(ntra)variant (some operation) and co(ntra)variant (swap (some operation)) (not just here, everywhere, I would say). I wonder if we could get mul_opposites to take care of such things. E.g, if a type R satisfies covariant_class R R (*) (<) then R^op satisfies covariant_class R R (swap (*)) (<).

[adomani]

Anyway, in case this is relevant, it would be for a separate PR!

LGTM!

[b-mehta]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests