Zulip Chat Archive

Stream: PR reviews

Topic: 2844


view this post on Zulip Yury G. Kudryashov (Jun 09 2020 at 20:39):

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?

view this post on Zulip Johan Commelin (Jun 09 2020 at 20:47):

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.

view this post on Zulip Johan Commelin (Jun 09 2020 at 20:48):

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.

view this post on Zulip Johan Commelin (Jun 09 2020 at 20:48):

Then we would get other examples besides nnreal.


Last updated: May 09 2021 at 12:14 UTC