Lean mathlib documentation
Navigate through mathlib files using the menu on the right.
Declaration names link to their locations in the mathlib or core Lean source. Names inside code snippets link to their locations in this documentation.
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.