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.
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.
Group theory group, group morphism, subgroup, subgroup generated by a subset, quotient group, first isomorphism theorem, abelianization, free group, group action, cyclic group, permutation group of a type.
Divisibility in integral domains irreducible elements, coprime elements, unique factorisation domain, greatest common divisor, least common multiple, principal ideal domain, Euclidean domains, Euclid's' algorithm, Euler's totient function ($\varphi$), sums of two squares, sums of four squares, quadratic reciprocity, 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]$ is a UFD when $A$ is a UFD, irreducible polynomial, Eisenstein's criterion, polynomial in several indeterminates, Chevalley-Warning theorem, power series, Hensel's lemma.
Field theory fields, characteristic of a ring, characteristic zero, characteristic p, Frobenius morphisms, algebraically closed field, exitence of algebraic closure of a field, $\C$ is algebraically closed, field of fractions of an integral domain, algebraic extensions, rupture field, splitting field, perfect closure.
Bilinear and quadratic forms bilinear forms, alternating bilinear forms, symmetric bilinear forms, matrix representation, quadratic form, polar form of a quadratic, Euclidean vector spaces, Cauchy-Schwarz inequality, self-adjoint endomorphism.
See also our documentation page about linear algebra.
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 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, 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 functions, contraction mapping theorem, Baire theorem, Arzela-Ascoli theorem, Hausdorff distance, Gromov-Hausdorff space.
See also our documentation page about topology.
Normed vector 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), continuous linear maps, norm of a continuous linear map, 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.
Differentiability differentiable functions between normed vector spaces, derivative of a composition of functions, derivative of the inverse of a function, Rolle's theorem, mean value theorem, $C^k$ functions, Leibniz formula, local extrema, inverse function theorem, implicit function theorem, analytic function.
Measures and integral calculus sigma-algebras, measurable functions, the category of measurable space, Borel sigma-algebras, positive measure, Lebesgue measure, Giry monad, integral of positive measurable functions, monotone convergence theorem, Fatou's lemma, vector-valued integrable functions (Bochner integral), $L^1$ space, Bochner integral, dominated convergence theorem, fundamental theorem of calculus, part 1, Fubini's theorem.