[Merged by Bors] - feat(algebra/ordered_monoid): min_*_distrib

[pechersky]

Also provide a canonically_linear_ordered_add_monoid instances for nat, nnreal, cardinal and with_top.

---

I don't need the max versions, but someone could write those.

[bryangingechen]

Do you mind adding canonically_linear_ordered_add_monoid instances for nnreal, ennreal and cardinal as well?

edit: added some more examples

[pechersky]

Do you mind adding canonically_linear_ordered_add_monoid instances for nnreal, ennreal and cardinal as well?

edit: added some more examples

Added -- but I don't understand why the cardinal one needs noncomputable when the instances above it, that also rely on cardinal.linear_order, are not noncomputable.

[pechersky]

Somehow, the derive canonically_linear_ordered_add_monoid broke a proof later on. This might have to do with the weird diamond that Yury commented on in the file. But I don't know how to debug that.

[bryangingechen]

@pechersky @RemyDegenne The plan is to merge https://github.com/leanprover-community/mathlib/tree/ennreal_lattice_issue into this PR if it builds, right?

[RemyDegenne]

We could also merge this first. The other branch should build but it has some weird behaviour that I don't understand, and it may take a while to fix. canonically_linear_ordered_add_monoid verifies all properties of a semilattice_sup_bot but I cannot find a way to make lemmas on semilattice_sup_bot usable for it. Either I end up with two sup or with two bot.

[eric-wieser]

My opinion is that we should just merge this one.

[bryangingechen]

OK, thanks everyone!
bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

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