Package not recognized

Stream: new members

[DrGracePatty]

I installed according to instructions and created project, but for some reason the compiler won't recognize the Mathlib package when I include the 'import Mathlib' statement in my file.

[Notification Bot]

This topic was moved here from #lean4 > Package not recognized by Riccardo Brasca.

[Riccardo Brasca]

Have you opened the project folder in VSCode (rather than the single file or any other folder)?

[Kevin Buzzard]

If Riccardo's post doesn't answer your question then can you send a screenshot of your VS Code showing the error and with the file explorer open? I attach what this looks like on my machine:

example.png