R is the unique complete archimedean ordered field

Stream: Is there code for X?

[Kevin Buzzard]

Have we got some well-defined class referred to informally as "a complete archimedean ordered field" structure on an ID (say), and some equiv between is_CAOF X and X \equiv R? I think the last time I asked this the answer was that it was partly there.

[Reid Barton]

It seems to still be partly here, or more specifically, here: #3292

[Kevin Buzzard]

@Alex J. Best what is the situation with this? I'd like this stuff done for a forthcoming blog post (and hence am motivated to work on it myself)

[Alex J. Best]

I haven't had much lean time recently. I think the code is in good shape there are some comments Johan left on the pr that need adressing and some things in mathlib have changed since I last checked out that branch. I have marked it as please adopt so if you have motivation to do any of these things please go ahead! The only major mathematical thing was to prove uniqueness of the constructed map. I.e. there is only one order preserving ring hom between two of these fields. And a real cast to from the reals to these fields could be defined.

[Alex J. Best]

I would love to fix it at some point soon but have no immediate plans to do so unfortunately.

[Kevin Buzzard]

That's fine, I just wanted to check that the conflict wasn't some fatal thing or whatever

[Alex J. Best]

Oh no not at all. Most comments are small it just needs some TLC