Skip to main content

Documentation Index

Fetch the complete documentation index at: https://mintlify.com/leanprover-community/mathlib4/llms.txt

Use this file to discover all available pages before exploring further.

Mathlib4 is structured as a collection of more than 8,000 individual Lean 4 modules, each corresponding to a single .lean source file. These modules are organized into 31 subdirectories and 2 standalone files under the Mathlib/ folder (33 top-level entries in total), and every module is re-exported from the single root file Mathlib.lean. Understanding this hierarchy helps you import only what your project needs, keeps build times fast, and makes it easier to locate specific definitions and theorems in the library.

​
How the Module System Works

In Lean 4, every .lean file defines a module whose name matches its file path relative to the package root. For example, the file Mathlib/Algebra/Group/Defs.lean corresponds to the module Mathlib.Algebra.Group.Defs. Modules explicitly list their dependencies at the top of the file using import statements. The top-level Mathlib.lean file imports every module in the library via a flat list of public import directives: 
-- Mathlib.lean (excerpt)
module  -- shake: keep-all --deprecated_module: ignore

public import Std
public import Batteries
public import Mathlib.Algebra.AddConstMap.Basic
public import Mathlib.Algebra.AddConstMap.Equiv
-- ... 8000+ further imports
When you write import Mathlib in your project, you pull in everything. For faster compilation and a smaller dependency footprint, prefer selective imports.

​
Selective Imports

Instead of importing the entire library, you can import only the modules you actually use: 
-- Import just the basic group definitions
import Mathlib.Algebra.Group.Defs

-- Import ring theory basics
import Mathlib.RingTheory.Ideal.Basic

-- Import real analysis essentials
import Mathlib.Analysis.SpecialFunctions.Pow.Real
Selective imports dramatically reduce incremental build times during development. Start with a specific import and broaden it only if the elaborator cannot find the declarations you need.
If you are unsure which module contains a particular declaration, use the exact? or apply? tactics inside a proof, or search the online documentation by name.

​
Top-Level Directories

The 33 top-level entries in Mathlib/ each group a coherent area of mathematics or infrastructure. The cards below describe what each one contains.

Algebra

Algebraic structures: groups, rings, fields, modules, and algebras. Includes monoids, semirings, ordered algebraic types, and the BigOperators notation for ∑ and ∏.

AlgebraicGeometry

Schemes, sheaves of rings, morphisms of varieties, and the foundations of modern algebraic geometry following Grothendieck’s language.

AlgebraicTopology

Simplicial sets and simplicial complexes, homology, the singular simplicial set of a topological space, and related constructions.

Analysis

Real and complex analysis, measure theory, functional analysis, normed spaces, inner product spaces, and special functions such as exp, log, and trigonometric functions.

CategoryTheory

Categories, functors, natural transformations, adjunctions, limits and colimits, Yoneda lemma, abelian categories, and sheaves in categorical language.

Combinatorics

Graph theory, enumerative combinatorics, Ramsey theory, Young tableaux, and related discrete mathematics.

Computability

Turing machines, the halting problem, computability theory, and formal language theory.

Condensed

Condensed mathematics in the style of Clausen–Scholze: condensed sets, condensed abelian groups, and their basic properties.

Control

Monad transformer infrastructure: StateT, ReaderT, WriterT, and related abstractions used throughout the Lean 4 metaprogramming layer.

Data

Standard data structures: lists, finsets, multisets, arrays, trees, Finsupp (finitely supported functions), and arithmetic on Nat, Int, Rat, and ZMod.

Dynamics

Topological dynamics: fixed points, minimal systems, and ergodic-theoretic foundations.

FieldTheory

Galois theory, algebraic closures, field extensions, separability, splitting fields, and finite fields.

Geometry

Euclidean geometry (distances, angles, triangles) and differential geometry (manifolds, tangent bundles, vector fields).

GroupTheory

Group theory beyond the basic Algebra hierarchy: free groups, group actions, Sylow theory, solvable groups, and presentations.

InformationTheory

Shannon entropy, Kullback–Leibler divergence, mutual information, and the basics of coding theory.

LinearAlgebra

Linear maps, matrices, determinants, eigenvalues, bilinear forms, the rank–nullity theorem, tensor products, and exterior algebras.

Logic

Propositional and first-order logic foundations, relational structures, and the interface between type theory and classical logic.

MeasureTheory

σ-algebras, measures, Lebesgue integration, L^p spaces, Radon–Nikodym theorem, and the foundations of probability via measure theory.

ModelTheory

First-order model theory: languages, structures, theories, completeness, and Löwenheim–Skolem theorems.

NumberTheory

Primes, Diophantine equations, modular arithmetic, Dirichlet characters, L-functions, and arithmetic in number fields.

Order

Partially ordered sets, lattices, complete lattices, Galois connections, filters, and order-theoretic topology.

Probability

Probability spaces, random variables, distributions, independence, conditional expectation, and limit theorems.

RepresentationTheory

Group representations over fields, characters, Schur’s lemma, and the representation ring.

RingTheory

Advanced ring theory: UFDs, PIDs, Noetherian rings, Dedekind domains, Witt vectors, and localization.

SetTheory

Set theory foundations, ordinals, cardinals, cofinality, and cardinal arithmetic.

Tactic

Proof automation tactics: ring, linarith, norm_num, positivity, polyrith, decide, and helpers for writing custom tactics.

Topology

Topological spaces, continuous maps, metric spaces, uniform spaces, filters, compactness, and connectedness.

Util

Shared internal utilities: reflection helpers, attribute infrastructure, and miscellaneous lemmas used across Mathlib itself.

Deprecated

Declarations that have been superseded and are kept temporarily for backwards compatibility. Files here import their replacements and re-export them under the old names, allowing downstream code time to migrate.

Lean

Metaprogramming utilities and extensions to the Lean 4 elaborator specific to Mathlib’s needs — attribute infrastructure, environment extensions, and reflection helpers not provided by Batteries.

Testing

Infrastructure for property-based and unit testing within Mathlib, complementing the plausible dependency. Contains helpers for writing and running #test blocks and plausible examples.

Init.lean (file)

A standalone file that bootstraps Mathlib’s initialization: sets up default instances, notation, and options before the rest of the library is imported.

Tactic.lean (file)

A standalone re-export file: import Mathlib.Tactic gives access to all Mathlib tactics without importing the entire library.

​
Finding a Specific Theorem

If you know what you are looking for conceptually but not which module it lives in, several tools can help.
When you have a goal open in a Lean 4 proof state, these tactics search the library for applicable lemmas:
-- Suggests exact lemmas that close the goal
exact?

-- Suggests lemmas that can be applied to make progress
apply?

-- Searches for a simp lemma that rewrites the goal
simp?
The #check, #where, and #print commands are invaluable when navigating the module tree in VS Code with the Lean 4 extension. Hover over any identifier to see its type and the module where it is defined.

Build docs developers (and LLMs) love

Get started for freeTalk to us