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 ec822277b5d9b0bf7149367297c131c9077dbfc6 and Lean commit ed6accfb611bbd28ef5b7e34361d2b58a366e2c9.

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.