Update docs for ordered mixins

Stream: new members

[Peter Hansen]

I have noticed that several docstrings in mathlib still describe the semibundled
Ordered* classes (e.g. OrderedSemiring, LinearOrderedField) even though they were deprecated almost a year ago and replaced with mixins like docs#IsOrderedAddMonoid and docs#IsOrderedRing.

The dated references occur in several files, but it seems especially noticeable in the former core
files for the deprecated classes:

• Algebra.Order.Ring.Defs
• Algebra.Order.Ring.Unbundled.Basic
• Algebra.Order.GroupWithZero.Unbundled.Defs
• Algebra.Order.Monoid.Unbundled.Defs

I am considering a documentation-only PR to update the module docstrings and typeclass descriptions
to reference the new mixins. For

• Algebra.Order.GroupWithZero.Unbundled.Defs
• Algebra.Order.Monoid.Unbundled.Defs

it seems to just need replacing the suggested "less granular typeclasses" from their deprecated
versions to the new ones. The files

• Algebra.Order.Ring.Defs
• Algebra.Order.Ring.Unbundled.Basic

contain almost identical docstrings. They list the ten deprecated Ordered* classes for rings and
then explain a hierarchy among them. With the current mixins, we only have two classes:
docs#IsOrderedRing and docs#IsStrictOrderedRing. I am not entirely sure what the best replacement is.
Should we replace the hierarchy section with a short explanation of how these mixins interact with
the different ring and order assumptions?

I am a relatively new contributor and have not written documentation before, but I would like to
take a stab at it unless this is something that should generally be left to maintainers.

[Ruben Van de Velde]

Thanks for flagging this; if you want to take a stab at updating the docs, that would be very welcome