Blueprint Summary
Overview
Total entries208completed: 208; deps incomplete: 0; sorries: 0; no proof: 0
Ready now0Entries with an actionable next formalization step.
Fully closed208Local code and prerequisite closure are both complete.
Actionable priorities0Entries ready now and already unlocking downstream work.
Entry index (208)
Definitions56completed: 56; deps incomplete: 0; sorries: 0; no proof: 0
Propositions4completed: 4; deps incomplete: 0; sorries: 0; no proof: 0
Lemmas126completed: 126; deps incomplete: 0; sorries: 0; no proof: 0
Theorems21completed: 21; deps incomplete: 0; sorries: 0; no proof: 0
Corollaries1completed: 1; deps incomplete: 0; sorries: 0; no proof: 0
Definition Index (56)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (4)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (6)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (4)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (5)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (4)
-
Associated lean decls (4)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
Theorem / Proposition / Lemma / Corollary Index (152)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (4)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (2)
By parent groups (7)
Saddle geometry (13)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
Radial Mellin transform (9)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (2)
Mellin ansatz (10)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (4)
-
Associated lean decls (2)
Poisson inequality (10)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
Mellin-strip estimates (22)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
Comparison of the constants (18)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
Radial reduction (15)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (1)
Dependency insights
Statement-used entries84Entries reused in statement dependencies.
Proof-used entries151Entries reused in proof-only dependencies.
Tracked parent groups7Grouped health rollups for parents with more than one child entry.
Most used in statements (84)
-
Reverse dependencies recorded in statement dependencies.statement uses: 13proof uses: 0direct uses: 13downstream unlocks: 34
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 12proof uses: 0direct uses: 12downstream unlocks: 21
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 9proof uses: 0direct uses: 9downstream unlocks: 9
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 25
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 23
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 17
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 6proof uses: 10direct uses: 16downstream unlocks: 68
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 50
Associated lean decls (6)
-
Reverse dependencies recorded in statement dependencies.statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 42
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 37
Associated lean decls (1)
-
Show all 74 more statement-used entries
-
Reverse dependencies recorded in statement dependencies.statement uses: 6proof uses: 1direct uses: 7downstream unlocks: 36
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 29
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 26
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 22
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 20
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 6proof uses: 1direct uses: 7downstream unlocks: 11
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 6proof uses: 1direct uses: 7downstream unlocks: 9
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 45
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 20
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 19
Associated lean decls (4)
-
Reverse dependencies recorded in statement dependencies.statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 17
Associated lean decls (4)
-
Reverse dependencies recorded in statement dependencies.statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 12
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 1direct uses: 5downstream unlocks: 51
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 1direct uses: 5downstream unlocks: 30
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 30
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 25
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 22
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 19
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 19
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 1direct uses: 5downstream unlocks: 18
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 18
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 16
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 1direct uses: 5downstream unlocks: 12
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 11
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 37
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 1direct uses: 4downstream unlocks: 30
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 26
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 22
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 21
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 21
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 1direct uses: 4downstream unlocks: 20
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 19
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 3direct uses: 6downstream unlocks: 17
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 2direct uses: 5downstream unlocks: 14
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 12
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 2direct uses: 5downstream unlocks: 9
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 9
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 7
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 43
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 35
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 25
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 1direct uses: 3downstream unlocks: 18
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 17
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 2direct uses: 4downstream unlocks: 12
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 2direct uses: 4downstream unlocks: 12
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 10
Associated lean decls (5)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 1direct uses: 3downstream unlocks: 9
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 9
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 8
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 6
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 1direct uses: 3downstream unlocks: 2
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 2direct uses: 3downstream unlocks: 36
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 4direct uses: 5downstream unlocks: 35
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 30
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 3direct uses: 4downstream unlocks: 24
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 22
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 3direct uses: 4downstream unlocks: 16
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 2direct uses: 3downstream unlocks: 16
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 16
Associated lean decls (4)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 15
Associated lean decls (4)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 13
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 13
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 12
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 10
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 10
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 10
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 2direct uses: 3downstream unlocks: 9
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 9
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 3direct uses: 4downstream unlocks: 8
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 8
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 7
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 4
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 3
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 3
Associated lean decls (2)
-
Most used in proofs (151)
-
Reverse dependencies recorded in proof dependencies.proof uses: 10statement uses: 6direct uses: 16downstream unlocks: 68
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 8statement uses: 0direct uses: 8downstream unlocks: 32
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 5statement uses: 0direct uses: 5downstream unlocks: 6
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 4statement uses: 1direct uses: 5downstream unlocks: 35
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 4statement uses: 0direct uses: 4downstream unlocks: 15
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 4statement uses: 0direct uses: 4downstream unlocks: 14
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 4statement uses: 0direct uses: 4downstream unlocks: 14
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 3statement uses: 1direct uses: 4downstream unlocks: 24
-
Reverse dependencies recorded in proof dependencies.proof uses: 3statement uses: 3direct uses: 6downstream unlocks: 17
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 3statement uses: 0direct uses: 3downstream unlocks: 17
Associated lean decls (1)
-
Show all 141 more proof-used entries
-
Reverse dependencies recorded in proof dependencies.proof uses: 3statement uses: 1direct uses: 4downstream unlocks: 16
-
Reverse dependencies recorded in proof dependencies.proof uses: 3statement uses: 0direct uses: 3downstream unlocks: 15
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 3statement uses: 0direct uses: 3downstream unlocks: 14
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 3statement uses: 0direct uses: 3downstream unlocks: 14
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 3statement uses: 0direct uses: 3downstream unlocks: 11
-
Reverse dependencies recorded in proof dependencies.proof uses: 3statement uses: 0direct uses: 3downstream unlocks: 11
-
Reverse dependencies recorded in proof dependencies.proof uses: 3statement uses: 0direct uses: 3downstream unlocks: 10
Associated lean decls (4)
-
Reverse dependencies recorded in proof dependencies.proof uses: 3statement uses: 0direct uses: 3downstream unlocks: 10
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 3statement uses: 1direct uses: 4downstream unlocks: 8
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 3statement uses: 0direct uses: 3downstream unlocks: 3
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 1direct uses: 3downstream unlocks: 36
Associated lean decls (3)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 22
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 18
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 17
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 17
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 1direct uses: 3downstream unlocks: 16
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 15
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 15
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 15
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 15
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 15
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 15
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 3direct uses: 5downstream unlocks: 14
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 13
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 13
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 13
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 13
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 13
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 2direct uses: 4downstream unlocks: 12
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 2direct uses: 4downstream unlocks: 12
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 12
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 12
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 12
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 11
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 11
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 11
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 11
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 10
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 10
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 3direct uses: 5downstream unlocks: 9
Associated lean decls (3)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 1direct uses: 3downstream unlocks: 9
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 8
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 7
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 7
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 6
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 6
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 6
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 5
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 5
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 5
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 4
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 4
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 4
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 4
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 4direct uses: 5downstream unlocks: 51
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 6direct uses: 7downstream unlocks: 36
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 4direct uses: 5downstream unlocks: 30
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 3direct uses: 4downstream unlocks: 30
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 3direct uses: 4downstream unlocks: 20
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 4direct uses: 5downstream unlocks: 18
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 2direct uses: 3downstream unlocks: 18
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 17
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 16
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 16
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 16
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 16
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 16
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 16
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 16
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 16
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 16
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 15
Associated lean decls (4)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 15
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 15
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 14
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 14
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 14
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 14
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 13
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 13
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 13
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 4direct uses: 5downstream unlocks: 12
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 12
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 12
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 6direct uses: 7downstream unlocks: 11
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 11
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 11
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 10
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 10
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 10
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 10
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 10
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 10
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 10
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 10
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 10
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 6direct uses: 7downstream unlocks: 9
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 2direct uses: 3downstream unlocks: 9
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 9
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 9
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 9
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 9
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 9
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 9
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 9
Associated lean decls (3)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 9
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 9
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 8
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 8
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 8
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 8
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 8
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 7
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 7
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 7
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 7
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 6
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 6
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 5
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 4
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 4
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 4
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 3
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 3
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 3
Associated lean decls (3)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 3
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 3
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 3
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 2direct uses: 3downstream unlocks: 2
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
-
Group health (7)
-
Mellin ansatzGrouped view over entries sharing the same parent.total: 19closed: 19local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 420Next: no ready child currently unlocks downstream work.
-
Mellin-strip estimatesGrouped view over entries sharing the same parent.total: 29closed: 29local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 415Next: no ready child currently unlocks downstream work.
-
Saddle geometryGrouped view over entries sharing the same parent.total: 22closed: 22local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 343Next: no ready child currently unlocks downstream work.
-
Radial Mellin transformGrouped view over entries sharing the same parent.total: 13closed: 13local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 265Next: no ready child currently unlocks downstream work.
-
Poisson inequalityGrouped view over entries sharing the same parent.total: 13closed: 13local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 228Next: no ready child currently unlocks downstream work.
-
Radial reductionGrouped view over entries sharing the same parent.total: 18closed: 18local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 201Next: no ready child currently unlocks downstream work.
-
Comparison of the constantsGrouped view over entries sharing the same parent.total: 21closed: 21local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 93Next: no ready child currently unlocks downstream work.
Metadata
Metadata audit
Missing owner208
Missing effort208
Untagged208
Missing owner (208)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Show all 198 more entries missing owner
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (5)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (6)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (4)
-
Missing owner metadata.
Associated lean decls (4)
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (4)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (4)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (4)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing effort (208)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Show all 198 more entries missing effort
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (5)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (6)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (4)
-
Missing effort metadata.
Associated lean decls (4)
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (4)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (4)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (4)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Untagged (208)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Show all 198 more untagged entries
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (5)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (6)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (4)
-
Missing tag metadata.
Associated lean decls (4)
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (4)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (4)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (4)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Structure and coverage
Fully closed208Local code and ancestor closure are both complete.
Heaviest prerequisites (186)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 13statement deps: 3proof deps: 10direct uses: 1downstream unlocks: 9
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 9statement deps: 1proof deps: 8direct uses: 1downstream unlocks: 10
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 9statement deps: 3proof deps: 6direct uses: 2downstream unlocks: 11
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 9statement deps: 7proof deps: 2direct uses: 2downstream unlocks: 12
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 8statement deps: 1proof deps: 7direct uses: 2downstream unlocks: 13
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 8statement deps: 2proof deps: 6direct uses: 2downstream unlocks: 4
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 8statement deps: 4proof deps: 4direct uses: 1downstream unlocks: 12
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 8statement deps: 5proof deps: 3direct uses: 2downstream unlocks: 15
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 7statement deps: 1proof deps: 6direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 7statement deps: 2proof deps: 5direct uses: 1downstream unlocks: 15
Associated lean decls (1)
-
Show all 176 more heaviest-prerequisite entries
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 6statement deps: 2proof deps: 6direct uses: 2downstream unlocks: 7
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 6statement deps: 1proof deps: 5direct uses: 1downstream unlocks: 8
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 6statement deps: 1proof deps: 5direct uses: 1downstream unlocks: 10
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 6statement deps: 1proof deps: 5direct uses: 2downstream unlocks: 4
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 6statement deps: 1proof deps: 5direct uses: 1downstream unlocks: 2
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 6statement deps: 2proof deps: 4direct uses: 3downstream unlocks: 9
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 6statement deps: 2proof deps: 4direct uses: 2downstream unlocks: 10
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 6statement deps: 2proof deps: 4direct uses: 3downstream unlocks: 10
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 6statement deps: 3proof deps: 3direct uses: 3downstream unlocks: 11
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 6statement deps: 3proof deps: 3direct uses: 1downstream unlocks: 3
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 1proof deps: 5direct uses: 3downstream unlocks: 2
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 1proof deps: 4direct uses: 1downstream unlocks: 8
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 1proof deps: 4direct uses: 2downstream unlocks: 7
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 1proof deps: 4direct uses: 2downstream unlocks: 6
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 1proof deps: 4direct uses: 1downstream unlocks: 2
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 2proof deps: 3direct uses: 2downstream unlocks: 13
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 2proof deps: 3direct uses: 1downstream unlocks: 10
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 2proof deps: 3direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 2proof deps: 3direct uses: 0downstream unlocks: 0
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 2proof deps: 3direct uses: 1downstream unlocks: 1
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 2proof deps: 3direct uses: 1downstream unlocks: 3
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 3proof deps: 2direct uses: 1downstream unlocks: 10
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 3proof deps: 2direct uses: 2downstream unlocks: 13
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 4proof deps: 1direct uses: 4downstream unlocks: 16
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 1proof deps: 4direct uses: 2downstream unlocks: 3
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 1proof deps: 3direct uses: 4downstream unlocks: 8
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 1proof deps: 3direct uses: 1downstream unlocks: 13
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 1proof deps: 3direct uses: 2downstream unlocks: 15
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 1proof deps: 3direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 3proof deps: 2direct uses: 2downstream unlocks: 11
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 3proof deps: 2direct uses: 1downstream unlocks: 8
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 2proof deps: 2direct uses: 0downstream unlocks: 0
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 2proof deps: 2direct uses: 3downstream unlocks: 11
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 2proof deps: 2direct uses: 1downstream unlocks: 9
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 2proof deps: 2direct uses: 1downstream unlocks: 11
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 2proof deps: 2direct uses: 2downstream unlocks: 4
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 2proof deps: 2direct uses: 2downstream unlocks: 4
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 3proof deps: 1direct uses: 2downstream unlocks: 6
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 3proof deps: 1direct uses: 2downstream unlocks: 8
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 7downstream unlocks: 11
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 6downstream unlocks: 29
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 5downstream unlocks: 17
Associated lean decls (4)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 1downstream unlocks: 2
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 1proof deps: 3direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 0proof deps: 3direct uses: 2downstream unlocks: 10
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 0proof deps: 3direct uses: 1downstream unlocks: 7
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 2proof deps: 2direct uses: 0downstream unlocks: 0
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 2proof deps: 2direct uses: 2downstream unlocks: 8
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 2proof deps: 2direct uses: 0downstream unlocks: 0
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 1proof deps: 2direct uses: 1downstream unlocks: 14
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 1proof deps: 2direct uses: 3downstream unlocks: 14
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 1proof deps: 2direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 1proof deps: 2direct uses: 1downstream unlocks: 4
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 1proof deps: 2direct uses: 2downstream unlocks: 5
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 1proof deps: 2direct uses: 2downstream unlocks: 22
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 1proof deps: 2direct uses: 5downstream unlocks: 14
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 1proof deps: 2direct uses: 1downstream unlocks: 16
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 1proof deps: 2direct uses: 0downstream unlocks: 0
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 2proof deps: 1direct uses: 2downstream unlocks: 11
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 2proof deps: 1direct uses: 1downstream unlocks: 6
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 2proof deps: 1direct uses: 1downstream unlocks: 3
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 2proof deps: 1direct uses: 3downstream unlocks: 15
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 2proof deps: 1direct uses: 1downstream unlocks: 2
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 2proof deps: 1direct uses: 1downstream unlocks: 5
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 2downstream unlocks: 10
Associated lean decls (5)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 3downstream unlocks: 21
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 10
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 10
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 0proof deps: 2direct uses: 1downstream unlocks: 3
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 1direct uses: 2downstream unlocks: 15
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 1direct uses: 1downstream unlocks: 9
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 1direct uses: 1downstream unlocks: 16
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 1proof deps: 1direct uses: 2downstream unlocks: 9
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 1proof deps: 1direct uses: 1downstream unlocks: 14
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 1proof deps: 1direct uses: 3downstream unlocks: 17
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 1proof deps: 1direct uses: 4downstream unlocks: 12
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 1proof deps: 1direct uses: 4downstream unlocks: 14
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 1proof deps: 1direct uses: 5downstream unlocks: 9
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 1proof deps: 1direct uses: 2downstream unlocks: 13
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 1proof deps: 1direct uses: 1downstream unlocks: 10
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 1proof deps: 1direct uses: 2downstream unlocks: 12
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 1proof deps: 1direct uses: 2downstream unlocks: 13
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 1proof deps: 1direct uses: 2downstream unlocks: 10
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 1proof deps: 1direct uses: 2downstream unlocks: 6
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 1proof deps: 1direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 1proof deps: 1direct uses: 2downstream unlocks: 7
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 1proof deps: 1direct uses: 1downstream unlocks: 4
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 1proof deps: 1direct uses: 3downstream unlocks: 14
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 1proof deps: 1direct uses: 1downstream unlocks: 16
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 1proof deps: 1direct uses: 1downstream unlocks: 16
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 1proof deps: 1direct uses: 1downstream unlocks: 2
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 1proof deps: 1direct uses: 1downstream unlocks: 9
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 1proof deps: 1direct uses: 1downstream unlocks: 8
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 1proof deps: 1direct uses: 1downstream unlocks: 9
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 1proof deps: 1direct uses: 3downstream unlocks: 3
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 1proof deps: 1direct uses: 0downstream unlocks: 0
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 1proof deps: 1direct uses: 1downstream unlocks: 1
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 6downstream unlocks: 20
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 12downstream unlocks: 21
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 9downstream unlocks: 9
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 7downstream unlocks: 17
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 4downstream unlocks: 22
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 6downstream unlocks: 42
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 16
Associated lean decls (4)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 4downstream unlocks: 30
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 22
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 4downstream unlocks: 19
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 4downstream unlocks: 16
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 13
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 12
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 13
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 16
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 9
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 14
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 5
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 16
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 17
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 0proof deps: 1direct uses: 6downstream unlocks: 17
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 0proof deps: 1direct uses: 8downstream unlocks: 32
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 0proof deps: 1direct uses: 1downstream unlocks: 16
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 0proof deps: 1direct uses: 4downstream unlocks: 15
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 0proof deps: 1direct uses: 1downstream unlocks: 11
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 7downstream unlocks: 25
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 8
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 7
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 12
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 19
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 18
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 7downstream unlocks: 23
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 25
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 11
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 6
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 21
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 5downstream unlocks: 30
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 6downstream unlocks: 26
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 43
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 15
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 9
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 5downstream unlocks: 45
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 37
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 35
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 19
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 15
Associated lean decls (4)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 15
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 10
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 5downstream unlocks: 19
Associated lean decls (4)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 22
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 26
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 11
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 12
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 7downstream unlocks: 9
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 9
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 10
Associated lean decls (4)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 7
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 7
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 14
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 15
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 9
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 16
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 16
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 18
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 17
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 15
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 10
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 30
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 5downstream unlocks: 35
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 6
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 16
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 14
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 3
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 5downstream unlocks: 6
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 24
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 17
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 5
-
No prerequisites (22)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Show all 12 more entries without prerequisites
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (6)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
No dependents (10)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)