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

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

Trees tree, red-black tree, W type.

#### Logic and computation

Set theory ordinal, cardinal, model of ZFC.