## Stream: Is there code for X?

### Topic: R is the unique complete archimedean ordered field

#### Kevin Buzzard (Sep 08 2020 at 16:33):

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 (Sep 08 2020 at 16:40):

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

#### Kevin Buzzard (Sep 08 2020 at 16:44):

@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 (Sep 08 2020 at 16:47):

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 (Sep 08 2020 at 16:47):

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

#### Kevin Buzzard (Sep 08 2020 at 16:48):

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

#### Alex J. Best (Sep 08 2020 at 16:49):

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

Last updated: May 07 2021 at 18:19 UTC