jump to definition jumps to unimported file

Stream: lean4

[Kevin Buzzard]

On mathlib master, with Mathlib.Init.ZeroOne compiled, if I make a file containing this definition and no imports

-- no imports here
-- on mathlib master

class Zero (α : Type u) where
  zero : α

#check Zero

and then right click on Zero on the last #check line and then select "go to definition", my VS Code reliably takes me to a declaration in Mathlib.Init.ZeroOne. Indeed there is a definition of Zero there, it's just not been imported. Is this expected? Can anyone else reproduce? I'm on Ubuntu 22.04 and VS Code 1.74.2. Restarting VS Code and killing all lean processes on my machine doesn't help.