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 spaces, sheafed spaces, monoidal category, cartesian closed, abelian category. See also our documentation page about category theory.

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

Group theory group, group morphism, subgroup, subgroup generated by a subset, quotient group, first isomorphism theorem, abelianization, free group, group action, cyclic group, permutation group of a type.

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

Ideals and quotients ideal of a commutative ring, quotient rings, prime ideals, prime spectrum, Zariski topology, maximal ideals, Chinese remainder theorem, localization, fractional ideal.

Divisibility in integral domains irreducible elements, coprime elements, unique factorisation domain, greatest common divisor, least common multiple, principal ideal domain, Euclidean domains, Euclid's' algorithm, Euler's totient function ($\varphi$), sums of two squares, sums of four squares, quadratic reciprocity, 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, Chevalley-Warning theorem, power series, Hensel's lemma.

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

Field theory fields, characteristic of a ring, characteristic zero, characteristic p, Frobenius morphisms, algebraically closed field, exitence of algebraic closure of a field, $\C$ is algebraically closed, field of fractions of an integral domain, algebraic extensions, rupture field, splitting field, perfect closure.

Homological algebra chain complex, functorial homology.

Linear algebra

Fundamentals module, linear map, the category of modules over a ring, vector space, quotient space, tensor product, noetherian module, bases, multilinear 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 forms, alternating bilinear forms, symmetric bilinear forms, matrix representation, quadratic form, polar form of a quadratic, Euclidean vector spaces, 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.

Uniform notions uniform space, uniformly continuous functions, uniform convergence, Cauchy filters, Cauchy sequences, 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, 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 functions, 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 maps, norm of a continuous linear map, Banach open mapping theorem, absolutely convergent series in Banach spaces, Hahn-Banach theorem, dual of a normed space, isometric inclusion in double dual, completeness of spaces of bounded continuous functions.

Differentiability differentiable functions 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$ functions, Leibniz formula, local extrema, inverse function theorem, implicit function theorem, analytic function.

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

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

Measures and integral calculus sigma-algebras, measurable functions, the category of measurable space, Borel sigma-algebras, positive measure, Lebesgue measure, Giry monad, integral of positive measurable functions, monotone convergence theorem, Fatou's lemma, vector-valued integrable functions (Bochner integral), $L^1$ space, Bochner integral, dominated convergence theorem, fundamental theorem of calculus, part 1, Fubini's theorem.


Affine and Euclidean geometry affine spaces, affine functions, affine subspaces, barycenters, affine spans, Euclidean affine space, angles of vectors.

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

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

Data structures

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

Sets set, finite set, multiset.

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

Trees tree, red-black tree, W type.

Logic and computation

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

Set theory ordinal, cardinal, model of ZFC.