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 da66bb81bf0466335bae82077f0c335dfe53aeb3 and Lean commit 4c40c41ccc0820a4896255efa4b180c9922d8125.
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.