What does Lean already know?

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 I think mathematicians might be interested in.

Note that there are many other things within these libraries which I have not documented here (for example red black trees and so on);  these missing definitions and theorems may well be of interest to computer scientists. What is here is, of course, to a certain extent a reflection of my personal tastes.

Note that this page will necessarily age with time; the last time it was updated was 23rd Jan 2018. All the Lean code here should run with any version of Lean compiled on or after this date.


Rings and fields

Partial and total orders

Functions between types

Relations on types

Quotients and equivalence classes


The natural numbers

The integers.

To do: init/data/fin (certain finite sets) and all of mathlib (other than nat and int) [note that I have done most of mathlib “in rough”, it’s just a case of finding the time to type it up here.]