How to import a lean file?

Stream: lean4

[WangBoYu]

I'm new to lean, I want import some theorem in my file ./e1.lean, but when I write
import e1
lean seems not search the current path and remind me
unknown module prefix 'e1'
what should I do (

[Kevin Buzzard]

import MyProjectName.e1 maybe?

[Chris Bailey]

Are you in a lean project made with lake new/lake init (or a clone of an existing repo)? The basic set of files you get from those commands shows you how to import a file. Import statements are relative to the root, not the file. So if you have a file Data/Tree/Defs.lean and you want to import it in Data/Tree/Lemmas.lean, you need to write import Data.Tree.Defs at the top of Lemmas.lean.

[WangBoYu]

omg, it turns out that lake init is a necessary operation...