# Zulip Chat Archive

## 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)?

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

I'm giving a lecture about this in 90 minutes ;-)

#### 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