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 07fc9821f41bd369d930fa9ff8e83e56935e7594 and Lean commit de35266fe59614a98ea8a3460a158583fde4fa0d.
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.