Library reference
Declarations and API
The independent theorem and its numerical interfaces are the starting points for readers using the library.
| Declaration under MagnitudeConjecture | Purpose |
|---|---|
Statement.mainClaim | Full independent theorem, including nonsingularity |
Statement.isSpecialBiserial_iff | Exact equivalence of independent and production predicates |
RightModule.magnitudeConjecture_simpleCount | Full theorem with a direct simple-module count |
RightModule.simpleModuleCount_eq_numberOfSimpleModules | Connection with the original projective-count interface |
RightModule.FiniteIndecomposableSkeleton.projectiveLabelEquivSimpleLabel | The simple-top bijection over any field |
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.