[Merged by Bors] - docs(Algebra/Order/Ring/Defs): tiny IsDomain corrections

[madvorak]

---

Please check whether the new version is a correct description.

[alexjbest]

Actually it might be better to emphasize that IsDomain is a mixin now and not part of the heierachy. So it's not actually a predecessor in a literal sense

[madvorak]

Would you remove IsDomain from the comments, or change the wording?

[alexjbest]

I would change the wording to Ring + IsDomain with linear order (or whatever the correct version is)

[madvorak]

I couldn't make sense out of it (i.e., I didn't find a combination IsDomain + something where IsDomain wouldn't be redundant for given purposes). If you find something, please, fill it in; otherwise, I better delete these two lines.

I am not saying it is ideal thing to do to the docs, but it is certainly better now than what there was before.

[YaelDillies]

It does make sense. I pushed a fix with the new appropriate description.

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[riccardobrasca]

Thanks!

bors d+

[mathlib-bors]

✌️ madvorak can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[madvorak]

Thank you @YaelDillies !

Shouldn't " & + respects ≤ & * respects < " be there as well?
I am not sure what exactly implies the rest of the properties.

[YaelDillies]

The point was to relate to non-order properties, so no it wouldn't make much sense.

[madvorak]

The point was to relate to non-order properties, so no it wouldn't make much sense.

Should it be removed from lines 68, 74, 81, 88 then?

[YaelDillies]

No, I mean the point of those two specific lines. Each item in a sublist removes one condition from the corresponding header. The ones about IsDomain are precisely removing the compatibility between algebraic and order operations.

[madvorak]

Sorry; it seems I don't understand what IsDomain does. If you are sure it is now correct, I will trust you and merge it as is.

[YaelDillies]

IsDomain just says that a * b = 0 → a = 0 ∨ b = 0. This is a consequence of linearity of the order + compatibility of the algebraic operations, but it is a purely algebraic condition.

[madvorak]

And what implies that + respects ≤ then?

[YaelDillies]

I think you are misunderstanding the point of this whole paragraph in the docs. It's supposed to answer questions of the form "I stated a lemma using LinearOrderedRing but never used the compatibility of * with ≤ for anything else than a * b = 0 → a = 0 ∨ b = 0. What should I do?", the answer to which would be "Use Ring + IsDomain + maybe LinearOrder".

[madvorak]

Yeah, I misunderstood it totally!

Should I merge it now as it is?

[YaelDillies]

The docstring did slightly go out of date (since Domain is no more) and I'm happy with this PR in its current form, so please do!

[madvorak]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style
• Check all files imported