# 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 pages about natural numbers, and $p$-adic 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 characteristic polynomial, Cayley-Hamilton theorem.

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

#### Geometry

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

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

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.