## Stream: maths

### Topic: Uniqueness of the reals

#### Kevin Buzzard (Oct 16 2019 at 08:28):

Does mathlib have the theorem that the reals is "the unique complete archimedean field" (this can be made precise)?

#### Mario Carneiro (Oct 16 2019 at 08:28):

the uniqueness is not proved

#### Mario Carneiro (Oct 16 2019 at 08:29):

we would need real.cast which hasn't been defined yet

#### Mario Carneiro (Oct 16 2019 at 08:30):

If you have any conditionally complete ordered division ring A I think you can define a function real.cast : real -> A by extending rat.cast continuously. I'm not sure if that's the best constraint

#### Mario Carneiro (Oct 16 2019 at 08:32):

If you had some kind of sequential completeness assumption, the function could probably be computable too

#### Mario Carneiro (Oct 16 2019 at 08:38):

I think you can use dense_embedding to extend rat.cast if you know complete_space A

#### Kevin Buzzard (Oct 16 2019 at 08:55):

I am not necessarily going to use much Lean in this lecture, but basically the more we have the merrier.

#### Kevin Buzzard (Oct 16 2019 at 08:55):

If you have any conditionally complete ordered division ring A I think you can define a function real.cast : real -> A by extending rat.cast continuously. I'm not sure if that's the best constraint

This sounds like a job for @Patrick Massot but he's probably popping the champagne after getting our paper finished ;-)

Last updated: May 12 2021 at 07:17 UTC