# Lean mathematical theories

The core Lean library (imported automatically) and mathlib, the
mathematics library, between them know quite a lot of basic
undergraduate-level mathematical definitions. This page is an overview
of the definitions and lemmas within these libraries that
mathematicians might be interested in.

Note that there are many other things within these libraries which
are not documented here (for example red black trees and so on); these
missing definitions and theorems may well be of interest to computer
scientists.

* [Functions between types](theories/functions.md)
* [Relations on types, quotients](theories/relations.md)
* [Partial and total orders, lattices](theories/orders.md)
* [Sets and set like objects](theories/sets.md)
* [Categories](theories/category_theory.md)
* [The natural numbers](theories/naturals.md)
* [The integers](theories/integers.md)
* [Groups](theories/groups.md)
* [Rings and fields](theories/rings_fields.md)
* [Linear algebra](theories/linear_algebra.md)
* [Number theory](theories/number_theory.md)
* [Topological, uniform and metric spaces](theories/topology.md)
* [Measure theory](theories/measure.md)
