Getting "unknown identifier 'ℕ'" on #check ℕ

Stream: new members

[Ritobrata Ghosh]

I have done all the setup as mentioned in the getting started tutorials. But I am getting this error.

#check 2 works as expected.
But the same problem also persists for pi-

#check π

leads to

unknown identifier 'π'

But, instead of ℕ, if I use #check Nat, it works as expected, and I get- "Nat : Type".

What is this problem, and how do I resolve it?

[Kyle Miller]

The ℕ notation is defined in mathlib. You can get it if you import nearly anything from mathlib (provided you have mathlib as part of your project), and the minimal import is import Mathlib.Init.Data.Nat.Notation

[Kyle Miller]

It looks like the notation for docs#Real.pi comes from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic, and to activate it you further have to do open scoped Real

[Ritobrata Ghosh]

Kyle Miller said:

The ℕ notation is defined in mathlib.

I just did import Mathlib and restarted the file, and it worked very well.

Thanks for the help.