# 1.22 Imports and Dependencies

Imports control what a Lean file can see. Dependencies control what a Lean project can use. Together, they define the environment in which definitions, theorems, tactics, notation, and instances are resolved.

## Problem

You want to import declarations from other files, use external libraries, and keep project dependencies reproducible.

## Solution

Use `import` at the top of a Lean file.

```lean id="wsk25p"
import Std
```

This makes declarations from `Std` available in the current file.

For a local module:

```lean id="d1q2ne"
import Myproj.Basic
```

The module name must match the file path:

```text id="fm8l1s"
Myproj/Basic.lean
```

## Local Imports

Suppose your project contains:

```text id="mp8o0i"
Myproj/
├── Basic.lean
└── Extra.lean
```

In `Myproj/Basic.lean`:

```lean id="u3kyra"
namespace Myproj

def double (n : Nat) : Nat :=
  n + n

end Myproj
```

In `Myproj/Extra.lean`:

```lean id="p7k0rc"
import Myproj.Basic

#eval Myproj.double 10
```

Expected output:

```text id="r24v6k"
20
```

The import gives `Extra.lean` access to declarations compiled from `Basic.lean`.

## Imports Are Explicit

Lean does not search all files in a project automatically. If a declaration is in another module, import that module.

```lean id="syoa8l"
import Myproj.Basic
```

Without the import, Lean reports that the name is unknown.

This explicit model keeps dependencies visible and makes compilation predictable.

## Import Order

Imports usually appear before all declarations.

```lean id="zxt6q1"
import Std
import Myproj.Basic

namespace Myproj
```

The order matters when later imports depend on earlier ones, but ordinary files should avoid relying on subtle ordering effects. Prefer direct imports for the declarations you use.

## Transitive Imports

If module `A` imports `B`, and `B` imports `C`, then `A` can often see declarations from `C`.

However, relying on transitive imports makes files fragile. If `B` later stops importing `C`, then `A` may break.

Prefer direct imports for important dependencies.

```lean id="tjmq71"
import Myproj.C
import Myproj.B
```

This makes the file's requirements explicit.

## Module Paths

The import path follows the directory structure.

| File path                   | Import                        |
| --------------------------- | ----------------------------- |
| `Myproj/Basic.lean`         | `import Myproj.Basic`         |
| `Myproj/Data/List.lean`     | `import Myproj.Data.List`     |
| `Myproj/Algebra/Group.lean` | `import Myproj.Algebra.Group` |

The module name is case-sensitive. Keep directory names and module names aligned.

## Dependencies in Lake

External dependencies are declared in `lakefile.lean`.

A minimal Lake file:

```lean id="oe1but"
import Lake
open Lake DSL

package «myproj» where

lean_lib Myproj
```

To use an external dependency, add a `require` declaration.

```lean id="nrh61d"
require mathlib from git
  "https://github.com/leanprover-community/mathlib4"
```

Then run:

```sh id="rknzlr"
lake update
lake build
```

Lake records resolved dependencies in:

```text id="e1xxrp"
lake-manifest.json
```

Commit this file to make builds reproducible.

## The Toolchain File

The file `lean-toolchain` pins the Lean version.

Example:

```text id="eqmieb"
leanprover/lean4:stable
```

or:

```text id="bqvjbr"
leanprover/lean4:v4.12.0
```

When you run `lean` or `lake`, `elan` reads this file and chooses the matching toolchain.

For stable projects, prefer a specific version over `stable`.

## Importing Mathlib

After adding mathlib as a dependency, import it in Lean files.

```lean id="ju37g6"
import Mathlib
```

This imports a large library and can increase build and elaboration time.

Prefer smaller imports when possible:

```lean id="r4oz5n"
import Mathlib.Data.Nat.Basic
import Mathlib.Tactic
```

Small imports improve build performance and make dependencies clearer.

## Dependency Hygiene

Good import hygiene follows a few rules:

| Practice                               | Reason                                |
| -------------------------------------- | ------------------------------------- |
| Import what you use directly           | Avoid fragile transitive dependencies |
| Prefer smaller imports                 | Improve build time                    |
| Keep examples separate from core files | Avoid unnecessary dependencies        |
| Commit `lake-manifest.json`            | Preserve dependency versions          |
| Pin Lean versions                      | Reduce toolchain drift                |

## Diagnosing Import Errors

If Lean reports:

```text id="m3lur1"
unknown module prefix
```

check that:

* the file path matches the module name
* the file belongs to a declared `lean_lib`
* the project root is open in the editor
* `lake build` succeeds from the terminal

If Lean reports an unknown declaration after an import, the declaration may live in a different module. Use search tools in the editor or import the broader parent module temporarily.

## Cyclic Imports

Imports must form an acyclic graph. This is invalid:

```text id="kyz0gt"
A imports B
B imports A
```

Fix cycles by extracting shared declarations into a third module.

```text id="nps8sv"
Common
├── imported by A
└── imported by B
```

This keeps the dependency graph directed and compilable.

## Recipe: Split a File into Modules

Start with one file:

```text id="f2p2gv"
Myproj/Basic.lean
```

Move reusable definitions into:

```text id="po0p7x"
Myproj/Data.lean
```

Then import it:

```lean id="qjw12z"
import Myproj.Data
```

Keep theorem-heavy or example-heavy code in separate modules when possible.

## Common Pitfalls

If imports work in the terminal but fail in the editor, open the project root folder.

If imports work on one machine but fail on another, compare `lean-toolchain` and `lake-manifest.json`.

If a file depends on a declaration only through a transitive import, add the direct import.

If importing all of `Mathlib` slows development, replace it with narrower imports.

If two modules need each other, move shared declarations to a third module.

## Takeaway

Imports define the visible Lean environment for a file. Lake dependencies define the libraries available to the project. Keep imports explicit, module paths aligned with files, dependencies pinned, and the import graph acyclic. This gives Lean enough structure to compile predictably and gives readers enough information to understand where names come from.