The modules of FrcCore

The 137 modules of lean/FrcCore, the substrate from first principles, no Mathlib, no axioms, in the order the site renders them: 4249 theorems (4248 with no axioms, 0 at tier 1, 0 at tier 2, 1 red) and 1083 definitions. Each module's page renders it with an anchor per declaration and names the modules it rests on.

module	theorems	no axioms	red	definitions	rests on
Nat	46	46	0	1	0
Pigeonhole	9	9	0	4	1
Shell	52	52	0	3	1
Series	28	28	0	8	3
Cycle	7	7	0	1	4
Ring	17	17	0	16	2
FrameCore	42	42	0	6	4
Frame	19	19	0	3	5
Parity	9	9	0	0	5
Transform	20	20	0	4	6
Orbit	32	32	0	2	7
Sum	11	11	0	4	9
Theme/Projective	33	33	0	18	7
Theme/Lorentz	81	81	0	28	11
Theme/Register	8	8	0	6	14
Theme/Fourier	77	77	0	10	9
Theme/Fractional	112	112	0	0	10
Theme/Lifts	25	25	0	2	11
Theme/Dichotomy	35	35	0	1	12
Theme/Rotations	29	29	0	4	11
Theme/Heisenberg	29	29	0	3	14
Theme/Spectra	17	17	0	4	15
Theme/Exclusivity	31	31	0	0	16
Theme/Quadratic	25	25	0	7	3
Theme/Extension	49	49	0	40	8
Theme/Tally	8	8	0	23	0
Theme/Numbers	5	5	0	1	9
Theme/Logic	58	58	0	22	4
Theme/SecondOrder	4	4	0	4	5
Theme/Formation	37	37	0	14	5
Theme/Reach	40	40	0	26	5
Theme/Diagonal	31	31	0	15	6
Theme/Threshold	44	44	0	12	7
Theme/Sets	30	30	0	13	5
Theme/Equivariant	7	7	0	6	2
Theme/Transfer	21	21	0	7	6
Theme/Field	45	45	0	3	5
Theme/Foundation	18	18	0	3	7
Theme/Drive	19	19	0	1	6
Theme/Carrier	32	32	0	2	8
Theme/Subject	30	30	0	4	10
Theme/Pair	44	44	0	10	11
Theme/Hopf	6	6	0	0	10
Theme/Symbol	71	71	0	11	5
Theme/Gravity	61	61	0	10	7
Theme/Quantum	28	28	0	5	8
Theme/Unitary	88	88	0	25	4
Theme/Interactions	31	31	0	26	10
Theme/Fields	6	6	0	39	12
Theme/Horizon	31	31	0	5	14
Theme/Zeros	29	29	0	4	15
Theme/Shift	3	3	0	1	5
Theme/Lattice	5	5	0	5	6
Theme/Drift	36	36	0	4	12
Theme/Relaxation	10	10	0	5	14
Theme/Window	31	31	0	8	1
Theme/Static	17	17	0	5	16
Theme/Observation	49	49	0	3	11
Theme/Interference	14	14	0	4	7
Theme/Composite	39	39	0	1	12
Theme/Strata	23	23	0	19	1
Theme/Ladder	46	46	0	13	6
Theme/Flavour	41	41	0	7	12
Theme/Dark	16	16	0	2	13
Meridian	6	6	0	2	6
Fourier	26	26	0	0	23
Algebra	17	17	0	0	32
Epi	82	82	0	51	14
Dimensions	75	75	0	17	13
Poly	14	14	0	7	4
Quaternion	0	0	0	0	34
Causality	12	12	0	0	26
Representation	27	27	0	7	20
Reductio	43	43	0	18	20
Godel	51	51	0	19	14
Finitism	14	14	0	0	20
Geometry	19	19	0	0	23
Complex	0	0	0	0	14
Instances	8	8	0	0	8
Rh	60	60	0	12	24
Entropy	55	55	0	1	18
Dirac	49	49	0	0	33
Gravity	42	42	0	0	41
S13	37	37	0	0	29
Spacetime	50	50	0	0	39
Fields	55	55	0	0	23
Quantum	46	46	0	0	24
Pnp	12	12	0	0	26
Flavour	27	27	0	0	17
Dark	13	13	0	0	16
Keys/Frame	27	27	0	0	12
Keys/Extension	7	7	0	0	11
Keys/Projective	34	34	0	0	15
Keys/Fourier	23	23	0	0	17
Keys/Numbers	1	1	0	0	10
Keys/Logic	57	57	0	0	13
Keys/Foundation	8	8	0	0	10
Keys/Carrier	5	5	0	0	9
Keys/Subject	39	39	0	0	19
Keys/Gravity	43	43	0	0	23
Keys/Relaxation	14	14	0	0	19
Keys/Quantum	49	49	0	0	22
Keys/Interactions	37	37	0	0	13
Keys/Horizon	30	30	0	0	18
Keys/Flavour	26	26	0	0	14
Keys/Dark	13	13	0	0	15
Theme/Hadrons	19	19	0	53	13
Hadrons	43	43	0	0	16
Keys/Hadrons	48	48	0	0	15
Theme/Super	7	6	1	7	14
Keys/Super	2	2	0	0	16
Theme/Spin	37	37	0	35	10
Theme/Calibration	13	13	0	24	6
Theme/Dirac	42	42	0	50	14
Theme/Packed	60	60	0	28	1
Theme/Plane	12	12	0	3	15
Theme/Hermitian	69	69	0	14	16
Theme/Operator	117	117	0	10	10
Theme/Unipotent	21	21	0	2	12
Theme/Spinor	30	30	0	37	21
Theme/Loss	10	10	0	4	2
Theme/Det	91	91	0	16	17
Theme/Elim	45	45	0	13	19
Theme/Cayley	32	32	0	8	20
Theme/Product	52	52	0	16	21
Theme/Poly	25	25	0	10	17
Theme/CharPoly	41	41	0	16	23
Keys/Dirac	19	19	0	0	15
Keys/Operator	28	28	0	0	27
Theme/Domain	7	7	0	22	0
Keys/Domain	1	1	0	0	1
Theme/Framed	40	40	0	8	13
Theme/Quaternion	37	37	0	5	16
Keys/Algebra	8	8	0	0	18
Theme/Orbital	11	11	0	3	12
Theme/Cells	4	4	0	20	13
Theme/Causal	28	28	0	2	11