The 29 modules of lean/FrcMathlib, the framework on Mathlib: the paper modules and the chart theme, in the order the site renders them: 1404 theorems (44 with no axioms, 144 at tier 1, 1216 at tier 2, 0 red) and 118 definitions. Each module's page renders it with an anchor per declaration and names the modules it rests on.
| module | theorems | no axioms | tier 1 | tier 2 | red | definitions | rests on |
|---|---|---|---|---|---|---|---|
| Algebra | 29 | 0 | 1 | 28 | 0 | 0 | 13 |
| Fourier | 51 | 0 | 2 | 49 | 0 | 3 | 3 |
| Geometry | 18 | 0 | 2 | 16 | 0 | 0 | 3 |
| Causality | 15 | 0 | 5 | 10 | 0 | 0 | 2 |
| Representation | 22 | 3 | 2 | 17 | 0 | 1 | 0 |
| Reductio | 24 | 1 | 2 | 21 | 0 | 3 | 2 |
| Epi | 186 | 17 | 12 | 157 | 0 | 19 | 0 |
| Dimensions | 117 | 2 | 28 | 87 | 0 | 31 | 2 |
| Rh | 44 | 0 | 4 | 40 | 0 | 0 | 11 |
| Entropy | 82 | 0 | 8 | 74 | 0 | 2 | 10 |
| Dirac | 102 | 0 | 12 | 90 | 0 | 1 | 4 |
| Gravity | 68 | 0 | 3 | 65 | 0 | 1 | 11 |
| Godel | 27 | 0 | 1 | 26 | 0 | 3 | 2 |
| S13 | 10 | 0 | 0 | 10 | 0 | 0 | 11 |
| Fields | 14 | 0 | 0 | 14 | 0 | 0 | 10 |
| Flavour | 35 | 0 | 0 | 35 | 0 | 0 | 10 |
| Quantum | 28 | 0 | 10 | 18 | 0 | 0 | 11 |
| Pnp | 7 | 0 | 0 | 7 | 0 | 0 | 10 |
| Spacetime | 4 | 0 | 0 | 4 | 0 | 0 | 12 |
| Dark | 45 | 0 | 0 | 45 | 0 | 0 | 10 |
| Hadrons | 69 | 0 | 0 | 69 | 0 | 0 | 2 |
| Theme/Chart | 53 | 0 | 0 | 53 | 0 | 4 | 1 |
| Theme/Strong | 35 | 0 | 0 | 35 | 0 | 0 | 2 |
| Theme/Gravity | 15 | 0 | 5 | 10 | 0 | 1 | 0 |
| Theme/Lorentz | 5 | 0 | 0 | 5 | 0 | 3 | 0 |
| Theme/Dirac | 141 | 21 | 42 | 78 | 0 | 46 | 2 |
| Keys/Chart | 105 | 0 | 0 | 105 | 0 | 0 | 9 |
| Keys/Gravity | 9 | 0 | 0 | 9 | 0 | 0 | 1 |
| Keys/Dirac | 44 | 0 | 5 | 39 | 0 | 0 | 3 |