unknown identifier 'ℚ'

Stream: mathlib4

[Attila Vajda]

Hello, pls help, I made new project with Project: Make Project With Mathlib. But for

example : ℚ := 1

there is error unknown identifier 'ℚ'

I would like to learn theorem solving from one of the tutorials, and I am using VS Code.

[Attila Vajda]

in Proj.lean importing import Mathlib.Data.Rat doesn't find the file, and I'm not sure which module to import for ℚ, if any at all

[Johan Commelin]

import Mathlib.Data.Rat.Init

should help. That's where the notation for Rat is defined.

[Attila Vajda]

Thank you @Johan Commelin

[Patrick Massot]

Which tutorial are you reading? It probably requires an update.