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

#### Linear algebra

Duality dual vector space, dual basis.

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

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

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

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