# 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.

Homological algebra chain complex, functorial homology.

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

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

#### Linear algebra#

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.

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.

#### Analysis#

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

Distribution theory Schwartz space.

#### Probability Theory#

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

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.

#### Dynamics#

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.

#### Logic and computation#

Set theory ordinal, cardinal, model of ZFC.