mathlib documentation


Navigate through mathlib files using the menu on the left.

Declaration names link to their locations in the mathlib or core Lean source. Names inside code snippets link to their locations in this documentation.

This documentation has been generated with mathlib commit 1e43208ed4bf7887eec843509aa99ed418f40cfe and Lean commit a5822ea47ebc52eec6323d8f1b60f6ec025daf99.

Note: mathlib is still only partially documented, and this HTML display is still under development. We welcome pull requests on GitHub to update misleading or badly formatted doc strings, or to add missing documentation.