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.
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.]