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 5b75f5ac2a1897f514941f95665f83480959026b and Lean commit a0fb1e8c7ac81dfd2e80ad0de08f4e57ee853d82.

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.