Library reference
Declarations and API
The independent theorems and the main library theorems are the starting points for readers using the library.
| Declaration under MultiplicativeBasisDeformations | Purpose |
|---|---|
Statement.theoremA | Theorem A in the independent vocabulary |
Statement.theoremB | Theorem B in the independent vocabulary |
Statement.translateCompatible | The translate defined by almost split sequences is the translation of the library |
theoremA | Theorem A in the library vocabulary |
theoremB | Theorem B in the library vocabulary |
awayFromTwoBasis | Corollary 5.5: the ray basis outside characteristic two |
standard_iff_rayLinearization | Theorem 11.8(2): A is standard exactly when A is isomorphic to k ray A |
Generated documentation
Browse and search the generated API
The API is generated by a separate pinned doc-gen4 project. The proof package itself depends only on Mathlib.