A mathlib overview

The goal of this web page is to give a rough list of topics currently covered in mathlib, and provide pointers for exploration. This is not meant to be an exhaustive list, and could be outdated (see the full index for exhaustive and up to date information).

Here topics are listed in the greatest generality we currently have in mathlib, hence some things may be difficult to recognize. We also have a page dedicated to undergraduate mathematics which may be easier to read, as well as a page listing undergraduate maths topics that are not yet in mathlib.

To make updates to this list, please make a pull request to mathlib after editing the yaml source file. This can be done entirely on GitHub, see "Editing files in another user's repository".

General algebra

Category theory category, small category, functor, natural transformation, Yoneda embedding, adjunction, monad, comma category, limits, presheafed space, sheafed space, monoidal category, cartesian closed, abelian category. See also our documentation page about category theory.

Numbers natural number, integer, rational number, continued fraction, real number, extended real number, complex number, $p$-adic number, $p$-adic integer, hyper-real number. See also our documentation page about natural numbers.

Group theory group, group morphism, group action, class formula, Burnside lemma, subgroup, subgroup generated by a subset, quotient group, first isomorphism theorem, second isomorphism theorem, third isomorphism theorem, abelianization, free group, presented group, cyclic group, nilpotent group, permutation group of a type.

Rings ring, ring morphism, the category of rings, subring, localization, local ring, noetherian ring, ordered ring.

Ideals and quotients ideal of a commutative ring, quotient ring, prime ideal, maximal ideal, Chinese remainder theorem, fractional ideal, first isomorphism theorem for commutative rings.

Divisibility in integral domains irreducible element, coprime element, unique factorisation domain, greatest common divisor, least common multiple, principal ideal domain, Euclidean domain, Euclid's' algorithm, Euler's totient function ($\varphi$), Lucas-Lehmer primality test.

Polynomials and power series polynomial in one indeterminate, roots of a polynomial, multiplicity, separable polynomial, $K[X]$ is Euclidean, Hilbert basis theorem, $A[X]$ has gcd and lcm if $A$ does, $A[X]$ is a UFD when $A$ is a UFD, irreducible polynomial, Eisenstein's criterion, polynomial in several indeterminates, power series.

Algebras over a ring associative algebra over a commutative ring, the category of algebras over a ring, free algebra of a commutative ring, tensor product of algebras, tensor algebra of a commutative ring, Lie algebra, exterior algebra, Clifford algebra.

Field theory field, characteristic of a ring, characteristic zero, characteristic p, Frobenius morphism, algebraically closed field, existence of algebraic closure of a field, $\C$ is algebraically closed, field of fractions of an integral domain, algebraic extension, rupture field, splitting field, perfect closure, Galois correspondence, Abel-Ruffini theorem (one direction).

Homological algebra chain complex, functorial homology.

Number theory sum of two squares, sum of four squares, quadratic reciprocity, solutions to Pell's equation, Matiyasevič's theorem, arithmetic functions, Bernoulli numbers, Chevalley-Warning theorem, Hensel's lemma (for $\mathbb{Z}_p$), ring of Witt vectors, perfection of a ring.

Transcendental numbers Liouville's theorem on existence of transcendental numbers.

Linear algebra

Fundamentals module, linear map, the category of modules over a ring, vector space, quotient space, tensor product, noetherian module, basis, multilinear map, alternating map, general linear group.

Duality dual vector space, dual basis.

Finite-dimensional vector spaces finite-dimensionality, isomorphism with $K^n$, isomorphism with bidual.

Matrices ring-valued matrix, matrix representation of a linear map, determinant, invertibility.

Endomorphism polynomials minimal polynomial, characteristic polynomial, Cayley-Hamilton theorem.

Structure theory of endomorphisms eigenvalue, eigenvector, existence of an eigenvalue.

Bilinear and quadratic forms bilinear form, alternating bilinear form, symmetric bilinear form, matrix representation, quadratic form, polar form of a quadratic, Euclidean vector space, Cauchy-Schwarz inequality, self-adjoint endomorphism.

See also our documentation page about linear algebra.


General topology filter, limit of a map with respect to filters, topological space, continuous function, the category of topological spaces, induced topology, open map, closed map, closure, cluster point, Hausdorff space, sequential space, extension by continuity, compactness in terms of filters, compactness in terms of open covers (Borel-Lebesgue), connectedness, compact open topology, Stone-Cech compactification, topological fiber bundle, Urysohn's lemma, Stone-Weierstrass theorem.

Uniform notions uniform space, uniformly continuous function, uniform convergence, Cauchy filter, Cauchy sequence, completeness, completion, Heine-Cantor theorem.

Topological algebra order topology, intermediate value theorem, extreme value theorem, limit infimum and supremum, topological group, completion of an abelian topological group, infinite sum, topological ring, completion of a topological ring, topological module, weak-* topology, Haar measure on a locally compact Hausdorff group.

Metric spaces metric space, ball, sequential compactness is equivalent to compactness (Bolzano-Weierstrass), Heine-Borel theorem (proper metric space version), Lipschitz continuity, Hölder continuity, contraction mapping theorem, Baire theorem, Arzela-Ascoli theorem, Hausdorff distance, Gromov-Hausdorff space.

See also our documentation page about topology.


Normed vector spaces normed vector space over a normed field, topology on a normed vector space, equivalence of norms in finite dimension, finite dimensional normed spaces over complete normed fields are complete, Heine-Borel theorem (finite dimensional normed spaces are proper), continuous linear map, norm of a continuous linear map, Banach open mapping theorem, absolutely convergent series in Banach spaces, Hahn-Banach theorem, dual of a normed space, Fréchet-Riesz representation of the dual of a Hilbert space, isometric inclusion in double dual, completeness of spaces of bounded continuous functions.

Differentiability differentiable function between normed vector spaces, derivative of a composition of functions, derivative of the inverse of a function, Rolle's theorem, mean value theorem, $C^k$ function, Leibniz formula, local extrema, inverse function theorem, implicit function theorem, analytic function.

Convexity convex function, characterization of convexity, Jensen's inequality (finite sum version), Jensen's inequality (integral version), convexity inequalities, Carathéodory's theorem.

Special functions logarithm, exponential, trigonometric functions, inverse trigonometric functions, hyperbolic trigonometric functions, inverse hyperbolic trigonometric functions.

Measures and integral calculus sigma-algebra, measurable function, the category of measurable spaces, Borel sigma-algebra, positive measure, Stieltjes measure, Lebesgue measure, Hausdorff measure, Hausdorff dimension, Giry monad, integral of positive measurable functions, monotone convergence theorem, Fatou's lemma, vector-valued integrable function (Bochner integral), $L^p$ space, Bochner integral, dominated convergence theorem, fundamental theorem of calculus, part 1, fundamental theorem of calculus, part 2, Fubini's theorem, product of finitely many measures.


Affine and Euclidean geometry affine space, affine function, affine subspace, barycenter, affine span, Euclidean affine space, angle.

Differentiable manifolds smooth manifold (with boundary and corners), smooth map between manifolds, tangent bundle, tangent map, Lie group, sphere.

Algebraic geometry prime spectrum, Zariski topology, locally ringed space, scheme, Nullstellensatz.


Graph theory simple graph, degree-sum formula, matching, adjacency matrix.

Pigeonhole principles finite, infinite, strong pigeonhole principle.

Transversals Hall's marriage theorem.

See also our documentation page about set-like objects.


Circle dynamics translation number, translation numbers define a group action up to semiconjugacy, translation number defines a homeomorphism up to semiconjugacy.

General theory omega-limit sets, fixed points, periodic points.

Data structures

List-like structures list, array, buffer, difference list, lazy list, stream, sequence, weak sequence.

Sets set, finite set, multiset, ordered set.

Maps key-value map, red-black map, hash map, finitely supported function, finite map.

Trees tree, red-black tree, size-balanced binary search tree, W type.

Logic and computation

Computability computable function, Turing machine, halting problem, Rice theorem, combinatorial game.

Set theory ordinal, cardinal, model of ZFC.