2844

Stream: PR reviews

[Yury G. Kudryashov]

I should've asked this before #2844 was merged. @Johan Commelin could you please expand the docstring(s) of multiplicative versions with some explanation why we want these classes? E.g., are there any instances besides multiplicative M and nnreal?

[Johan Commelin]

Any valuation on a field K induces an ordering on K that will be an example. We used such instances explicitly in the perfectoid project for building the canonical valuation.

[Johan Commelin]

We didn't really work with valuations of higher rank so far, but it's conceivable that someone wants to work on them as soon as the language is available.

[Johan Commelin]

Then we would get other examples besides nnreal.