converting numbers between ℕ, ℚ and ℝ

Stream: new members

[Jia Ming Lim]

Hi, I'm Jia Ming. This sounds a little silly but I have no clue how to deduce 0<↑n from 0<(n : ℕ) :( I'm stuck on the Real Numbers Game proving that the rationals are dense in $\mathbb{R}$. I've almost got it but what seems like the simplest most obvious thing ever stopped me. It would be super helpful to know where I can learn exactly how Lean handles the conversion of numbers between types.

[Kevin Buzzard]

You shouldn't be playing that level, it's not ready :-)

[Kevin Buzzard]

But maybe norm_cast will help.

[Jia Ming Lim]

Ohhh no wonder, I was wondering why a lot of things seems to be missing

[Jia Ming Lim]

Thanks! I'll try that

[Kevin Buzzard]

The first 7 levels are ready.

[Johan Commelin]

@Jia Ming Lim

It would be super helpful to know where I can learn exactly how Lean handles the conversion of numbers between types.

This is exactly what will be one of the topics in the workshop tomorrow!

[Kevin Buzzard]

and "max" is ready: http://wwwf.imperial.ac.uk/~buzzard/xena/max_minigame/

[Jia Ming Lim]

Omg yeah I played that, so super fun

[Kevin Buzzard]

I'm a bit busy this week, but we'll have an abs minigame soon :-) We'll then get on to limits.

[Amos Turchet]

all these new games will kill my research in these next weeks :D

[Jia Ming Lim]

YES!!!!! THANK YOU ALL, I DID IT HAHAHAH my proof is super messy but it workssss <3