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, Schreier's lemma, cyclic group, nilpotent group, permutation group of a type, structure of fintely generated abelian groups.

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_i}]$ 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.

Representation theory representation, category of finite dimensional representations, character, orthogonality of characters.

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.

Finitely generated modules over a PID structure theorem.

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.

Finite-dimensional inner product spaces (see also Hilbert spaces, below) existence of orthonormal basis, diagonalization of self-adjoint endomorphisms.

See also our documentation page about linear algebra.

Topology#

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, topological vector 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, continuous linear map, 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.

Analysis#

Topological vector spaces local convexity, Bornology, weak-* topology for dualities.

Normed vector spaces/Banach 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), norm of a continuous linear map, Banach-Steinhaus theorem, 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.

Hilbert spaces Inner product space, over $R$ or $C$, Cauchy-Schwarz inequality, adjoint operator, self-adjoint operator, orthogonal projection, reflection, orthogonal complement, existence of Hilbert basis, eigenvalues from Rayleigh quotient, Fréchet-Riesz representation of the dual of a Hilbert space, Lax-Milgram theorem.

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, Taylor's 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), uniform integrability, $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, convolution, approximation by convolution, regularization by convolution, change of variables formula, divergence theorem.

Complex analysis Cauchy integral formula, Liouville theorem, maximum modulus principle, principle of isolated zeros, principle of analytic continuation, analyticity of holomorphic functions, Schwarz lemma, removable singularity, Phragmen-Lindelöf principle, fundamental theorem of algebra.

Distribution theory Schwartz space.

Probability Theory#

Definitions in probability theory probability measure, independent events, independent sigma-algebras, conditional probability, conditional expectation.

Random variables and their laws discrete law, probability density function, variance of a real-valued random variable, independence of random variables, Kolmogorov's $0$-$1$ law, mean of product of independent random variables, moment of a random variable, Bernoulli law.

Convergence of a sequence of random variables convergence in probability, $\mathrm{L}^p$ convergence, almost sure convergence, convergence in distribution, Markov inequality, Chebychev inequality, strong law of large numbers.

Stochastic Processes martingale, optional stopping theorem, stopping time, hitting time.

Geometry#

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.

Combinatorics#

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.

Dynamics#

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.

Model theory first-order structure, first-order formula, satisfiability, substructure, definable set, elementary embedding, Compactness theorem, Löwenheim-Skolem.