Zulip Chat Archive

Stream: new members

Topic: Natural to real


Daniil Homza (Aug 25 2022 at 15:12):

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 (Aug 25 2022 at 15:18):

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.


Last updated: Dec 20 2023 at 11:08 UTC