Lean 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 1c4a2966ef25ec82e65337022a0764e87a81d992 and Lean 3.5c commit e1fe877236cd0c7aa4a655bfc51675e17e2353f7.

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.