How to read this document

A reader interested in the mathematical content can read the chapters linearly and ignore the hyperlink annotations. A reader interested in the formalization can click any \lean{}-annotated statement to open the corresponding Lean declaration page in the doc-gen4 API reference. A reader interested in the dependency structure of the theorems can consult the automatically generated dependency graph at dep_graph_document.html, which renders the \uses{} edges declared throughout the document.