Natural to real

Stream: new members

[Daniil Homza]

Hi all,

Just quick question. I want to multiply real number and natural number, How can I transform natural number into real?

Thanks in advance!

[Yaël Dillies]

Simply do! Lean will insert a coercion for you, turning the natural into a real. If you get an error, you will need to type-ascript, by writing (n : ℝ) * r instead of n * r, for example.