Zulip Chat Archive

Stream: Is there code for X?

Topic: reals are unique


view this post on Zulip Kevin Buzzard (Aug 06 2020 at 16:08):

Did we ever get one or both of "two complete totally ordered archimedean fields are equiv" or "a complete totally ordered archimedean field is equiv to \R"?

view this post on Zulip Bryan Gin-ge Chen (Aug 06 2020 at 16:35):

I think this is in #3292 by @Alex J. Best.

view this post on Zulip Alex J. Best (Aug 06 2020 at 16:36):

Johan left me some great comments, but I haven't had much lean time to implement them yet

view this post on Zulip Alex J. Best (Aug 06 2020 at 16:55):

If anyone wants to make any changes feel free to do so by the way, I just haven't had the chance to myself and really don't have a strong opinion RE: naming and what files things should go in.


Last updated: May 16 2021 at 05:21 UTC