All 38,690 definitions of Mathlib (its functions, constants, types, structures,
classes and predicates; not its theorems, instances or tactics), on 111 pages by part of Mathlib.
Each has the wording that the symbol table gives it, 25,857 of them (functions and constants 22,276 of 31,877 · types 1,763 of 2,466 · predicates 1,818 of 4,347), written by
hand in mathlib.dkgf or made by definition-table.py from the definition's
docstring or name, with the arguments shown by their names; and its reading in English, 38,279
of them: the statement of the definition, with its definiens where it has one, read by Informath
as the statements on the other pages are, where a constant without a wording is shown symbolically.
Search below to find a definition's page; each name there links to Mathlib's documentation, which
has the docstring.
| part of Mathlib | definitions | pages |
|---|---|---|
| Mathlib.Algebra | 6,562 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 |
| Mathlib.AlgebraicGeometry | 976 | 1 2 3 |
| Mathlib.AlgebraicTopology | 1,270 | 1 2 3 4 |
| Mathlib.Analysis | 1,830 | 1 2 3 4 5 |
| Mathlib.Basic | 168 | 1 |
| Mathlib.CategoryTheory | 9,720 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 |
| Mathlib.Combinatorics | 956 | 1 2 3 |
| Mathlib.Computability | 481 | 1 2 |
| Mathlib.Condensed | 169 | 1 |
| Mathlib.Data | 2,247 | 1 2 3 4 5 6 |
| Mathlib.Dynamics | 81 | 1 |
| Mathlib.FieldTheory | 314 | 1 |
| Mathlib.Geometry | 655 | 1 2 |
| Mathlib.GroupTheory | 1,188 | 1 2 3 |
| Mathlib.InformationTheory | 9 | 1 |
| Mathlib.Init | 3 | 1 |
| Mathlib.LinearAlgebra | 1,675 | 1 2 3 4 5 |
| Mathlib.Logic | 439 | 1 2 |
| Mathlib.MeasureTheory | 737 | 1 2 |
| Mathlib.ModelTheory | 361 | 1 |
| Mathlib.NumberTheory | 804 | 1 2 3 |
| Mathlib.Order | 1,575 | 1 2 3 4 |
| Mathlib.Probability | 253 | 1 |
| Mathlib.RepresentationTheory | 559 | 1 2 |
| Mathlib.RingTheory | 2,370 | 1 2 3 4 5 6 |
| Mathlib.SetTheory | 220 | 1 |
| Mathlib.Topology | 3,068 | 1 2 3 4 5 6 7 8 |