Blueprint Summary
Overview
Total entries406completed: 102; deps incomplete: 253; sorries: 0; no proof: 0
Ready now9Entries with an actionable next formalization step.
Fully closed102Local code and prerequisite closure are both complete.
Actionable priorities5Entries ready now and already unlocking downstream work.
Actionable priorities (5)
-
Ready for statement work.stage: statementstatement: ready to formalizedirect uses: 9downstream unlocks: 287
-
Ready for statement work.stage: statementstatement: ready to formalizedirect uses: 28downstream unlocks: 70
-
Ready for statement work.stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 12
-
Ready for statement work.stage: statementstatement: ready to formalizedirect uses: 2downstream unlocks: 8
-
Ready for statement work.stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 2
Entry index (406)
Definitions406completed: 102; deps incomplete: 253; sorries: 0; no proof: 0
Informal-only entries51
Definition Index (406)
-
Associated lean decls (3)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (4)
-
Associated lean decls (2)
-
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 (3)
-
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 (4)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (3)
-
Associated lean decls (2)
-
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 (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 (3)
-
Associated lean decls (5)
-
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 (4)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (3)
-
Associated lean decls (3)
-
Associated lean decls (4)
-
Associated lean decls (2)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (3)
-
Associated lean decls (2)
-
Associated lean decls (4)
-
Associated lean decls (2)
-
Associated lean decls (4)
-
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 (3)
-
Associated lean decls (3)
-
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 (1)
-
Associated lean decls (2)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (5)
-
Associated lean decls (4)
-
Associated lean decls (1)
-
Associated lean decls (4)
-
Associated lean decls (4)
-
Associated lean decls (3)
-
Associated lean decls (5)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (4)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (3)
-
Associated lean decls (2)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (2)
-
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 (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (5)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (3)
-
Associated lean decls (3)
-
Associated lean decls (3)
-
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 (3)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (4)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
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 (3)
-
Associated lean decls (4)
-
Associated lean decls (3)
-
Associated lean decls (2)
-
Associated lean decls (4)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (5)
-
Associated lean decls (2)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (3)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (4)
-
Associated lean decls (4)
-
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 (1)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (5)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (4)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (4)
-
Associated lean decls (1)
-
Associated lean decls (4)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
Dependency insights
Statement-used entries300Entries reused in statement dependencies.
Most used in statements (300)
-
Reverse dependencies recorded in statement dependencies.statement uses: 95proof uses: 0direct uses: 95downstream unlocks: 175
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 83proof uses: 0direct uses: 83downstream unlocks: 113
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 36proof uses: 0direct uses: 36downstream unlocks: 51
Associated lean decls (4)
-
Reverse dependencies recorded in statement dependencies.statement uses: 29proof uses: 0direct uses: 29downstream unlocks: 89
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 28proof uses: 0direct uses: 28downstream unlocks: 70
-
Reverse dependencies recorded in statement dependencies.statement uses: 20proof uses: 0direct uses: 20downstream unlocks: 76
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 20proof uses: 0direct uses: 20downstream unlocks: 66
-
Reverse dependencies recorded in statement dependencies.statement uses: 19proof uses: 0direct uses: 19downstream unlocks: 76
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 16proof uses: 0direct uses: 16downstream unlocks: 282
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 16proof uses: 0direct uses: 16downstream unlocks: 184
Associated lean decls (1)
-
Show all 290 more statement-used entries
-
Reverse dependencies recorded in statement dependencies.statement uses: 16proof uses: 0direct uses: 16downstream unlocks: 67
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 15proof uses: 0direct uses: 15downstream unlocks: 193
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 15proof uses: 0direct uses: 15downstream unlocks: 95
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 13proof uses: 0direct uses: 13downstream unlocks: 221
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 13proof uses: 0direct uses: 13downstream unlocks: 56
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 13proof uses: 0direct uses: 13downstream unlocks: 28
-
Reverse dependencies recorded in statement dependencies.statement uses: 13proof uses: 0direct uses: 13downstream unlocks: 24
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 12proof uses: 0direct uses: 12downstream unlocks: 26
Associated lean decls (5)
-
Reverse dependencies recorded in statement dependencies.statement uses: 11proof uses: 0direct uses: 11downstream unlocks: 59
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 11proof uses: 0direct uses: 11downstream unlocks: 29
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 10proof uses: 0direct uses: 10downstream unlocks: 68
Associated lean decls (4)
-
Reverse dependencies recorded in statement dependencies.statement uses: 10proof uses: 0direct uses: 10downstream unlocks: 57
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 10proof uses: 0direct uses: 10downstream unlocks: 16
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 9proof uses: 0direct uses: 9downstream unlocks: 287
-
Reverse dependencies recorded in statement dependencies.statement uses: 9proof uses: 0direct uses: 9downstream unlocks: 122
-
Reverse dependencies recorded in statement dependencies.statement uses: 9proof uses: 0direct uses: 9downstream unlocks: 84
Associated lean decls (4)
-
Reverse dependencies recorded in statement dependencies.statement uses: 9proof uses: 0direct uses: 9downstream unlocks: 51
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 9proof uses: 0direct uses: 9downstream unlocks: 27
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 9proof uses: 0direct uses: 9downstream unlocks: 14
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 8proof uses: 0direct uses: 8downstream unlocks: 52
Associated lean decls (4)
-
Reverse dependencies recorded in statement dependencies.statement uses: 8proof uses: 0direct uses: 8downstream unlocks: 42
Associated lean decls (5)
-
Reverse dependencies recorded in statement dependencies.statement uses: 8proof uses: 0direct uses: 8downstream unlocks: 24
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 8proof uses: 0direct uses: 8downstream unlocks: 18
-
Reverse dependencies recorded in statement dependencies.statement uses: 8proof uses: 0direct uses: 8downstream unlocks: 17
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 211
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 68
-
Reverse dependencies recorded in statement dependencies.statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 53
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 29
-
Reverse dependencies recorded in statement dependencies.statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 25
-
Reverse dependencies recorded in statement dependencies.statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 21
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 19
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 11
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 7
-
Reverse dependencies recorded in statement dependencies.statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 7
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 85
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 67
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 51
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 37
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 29
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 24
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 13
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 11
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 10
-
Reverse dependencies recorded in statement dependencies.statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 153
Associated lean decls (5)
-
Reverse dependencies recorded in statement dependencies.statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 116
-
Reverse dependencies recorded in statement dependencies.statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 114
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 78
Associated lean decls (4)
-
Reverse dependencies recorded in statement dependencies.statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 41
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 40
Associated lean decls (4)
-
Reverse dependencies recorded in statement dependencies.statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 38
Associated lean decls (4)
-
Reverse dependencies recorded in statement dependencies.statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 22
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 21
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 17
-
Reverse dependencies recorded in statement dependencies.statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 15
Associated lean decls (2)
-
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: 5proof uses: 0direct uses: 5downstream unlocks: 11
-
Reverse dependencies recorded in statement dependencies.statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 11
-
Reverse dependencies recorded in statement dependencies.statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 10
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 8
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 8
-
Reverse dependencies recorded in statement dependencies.statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 7
-
Reverse dependencies recorded in statement dependencies.statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 7
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 284
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 223
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 146
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 116
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 77
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 63
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 47
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 46
Associated lean decls (4)
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 45
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 42
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 36
Associated lean decls (5)
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 34
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 33
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 33
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 32
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 30
Associated lean decls (2)
-
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: 27
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 25
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 19
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 15
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 12
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 12
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 9
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 6
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 6
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 6
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 6
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 5
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 283
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 100
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 80
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 34
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 33
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 32
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 30
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 30
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 29
-
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: 24
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 23
Associated lean decls (3)
-
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: 20
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 16
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 15
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 8
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 8
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 5
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 4
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 3
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 3
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 283
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 224
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 79
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 65
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 49
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 46
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 45
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 31
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 26
-
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: 0direct uses: 2downstream unlocks: 25
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 22
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 22
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 21
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 21
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 21
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 21
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 20
Associated lean decls (4)
-
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: 0direct uses: 2downstream unlocks: 13
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 13
Associated lean decls (4)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 12
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 10
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 9
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 9
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 9
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 8
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 8
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 8
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 8
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 6
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 6
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 5
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 5
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 5
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 5
Associated lean decls (4)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 4
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 4
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 3
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 3
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 3
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 3
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 194
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 123
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 123
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 117
Associated lean decls (4)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 115
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 69
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 68
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 64
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 64
Associated lean decls (4)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 44
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 43
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 39
Associated lean decls (4)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 38
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 37
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 33
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 31
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 30
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 30
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 30
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 27
Associated lean decls (3)
-
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: 0direct uses: 1downstream unlocks: 21
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 20
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 20
Associated lean decls (4)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 19
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 19
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 19
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 19
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 18
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 18
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 16
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 14
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 13
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 13
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 12
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 12
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 12
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 12
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 11
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 11
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 11
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 11
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 11
-
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: 0direct uses: 1downstream unlocks: 10
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 10
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 10
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 9
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 9
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 9
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 8
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 8
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 8
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 8
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 7
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 7
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 6
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 6
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 6
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 5
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
Associated lean decls (4)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
Associated lean decls (4)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (5)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (4)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
-
Metadata
Metadata audit
Missing owner406
Missing effort406
Untagged406
Missing owner (406)
-
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 (5)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (1)
-
Show all 396 more entries missing owner
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (2)
-
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.
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
-
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 (4)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (3)
-
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.
-
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 (4)
-
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.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (3)
-
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 (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (3)
-
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 (2)
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (2)
-
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 (3)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (5)
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
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.
-
Missing owner metadata.
Associated lean decls (4)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
-
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 (5)
-
Missing owner metadata.
-
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 (2)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
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 (1)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
-
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 (2)
-
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 (2)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (5)
-
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.
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 (1)
-
Missing owner metadata.
Associated lean decls (2)
-
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.
Associated lean decls (2)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (3)
-
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 (2)
-
Missing owner metadata.
-
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 (3)
-
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 (1)
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
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 (1)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
-
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 (1)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (4)
-
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.
-
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 (3)
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
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 (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 (2)
-
Missing owner metadata.
Associated lean decls (4)
-
Missing owner metadata.
Associated lean decls (4)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (2)
-
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 (3)
-
Missing owner metadata.
Associated lean decls (4)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (4)
-
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 (4)
-
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 (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.
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
-
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 (1)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (3)
-
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.
Associated lean decls (4)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (1)
-
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 (2)
-
Missing owner metadata.
Associated lean decls (4)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
-
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 (2)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (4)
-
Missing owner metadata.
-
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 (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 (4)
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (4)
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (4)
-
Missing owner metadata.
-
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 (4)
-
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 (1)
-
Missing owner metadata.
Associated lean decls (5)
-
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 (3)
-
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 (3)
-
Missing owner metadata.
Associated lean decls (4)
-
Missing effort (406)
-
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 (5)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (1)
-
Show all 396 more entries missing effort
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (2)
-
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.
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
-
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 (4)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (3)
-
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.
-
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 (4)
-
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.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (3)
-
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 (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (3)
-
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 (2)
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (2)
-
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 (3)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (5)
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
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.
-
Missing effort metadata.
Associated lean decls (4)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
-
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 (5)
-
Missing effort metadata.
-
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 (2)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
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 (1)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
-
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 (2)
-
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 (2)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (5)
-
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.
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 (1)
-
Missing effort metadata.
Associated lean decls (2)
-
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.
Associated lean decls (2)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (3)
-
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 (2)
-
Missing effort metadata.
-
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 (3)
-
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 (1)
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
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 (1)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
-
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 (1)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (4)
-
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.
-
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 (3)
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
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 (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 (2)
-
Missing effort metadata.
Associated lean decls (4)
-
Missing effort metadata.
Associated lean decls (4)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (2)
-
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 (3)
-
Missing effort metadata.
Associated lean decls (4)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (4)
-
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 (4)
-
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 (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.
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
-
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 (1)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (3)
-
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.
Associated lean decls (4)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (1)
-
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 (2)
-
Missing effort metadata.
Associated lean decls (4)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
-
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 (2)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (4)
-
Missing effort metadata.
-
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 (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 (4)
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (4)
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (4)
-
Missing effort metadata.
-
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 (4)
-
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 (1)
-
Missing effort metadata.
Associated lean decls (5)
-
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 (3)
-
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 (3)
-
Missing effort metadata.
Associated lean decls (4)
-
Untagged (406)
-
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 (5)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (1)
-
Show all 396 more untagged entries
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (2)
-
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.
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
-
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 (4)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (3)
-
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.
-
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 (4)
-
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.
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (3)
-
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 (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (3)
-
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 (2)
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (2)
-
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 (3)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (5)
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
-
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.
-
Missing tag metadata.
Associated lean decls (4)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
-
Missing tag metadata.
-
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 (5)
-
Missing tag metadata.
-
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 (2)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
-
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 (1)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
-
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 (2)
-
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 (2)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (5)
-
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.
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 (1)
-
Missing tag metadata.
Associated lean decls (2)
-
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.
Associated lean decls (2)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (3)
-
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 (2)
-
Missing tag metadata.
-
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 (3)
-
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 (1)
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
-
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 (1)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
-
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 (1)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (4)
-
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.
-
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 (3)
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
-
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 (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 (2)
-
Missing tag metadata.
Associated lean decls (4)
-
Missing tag metadata.
Associated lean decls (4)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (2)
-
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 (3)
-
Missing tag metadata.
Associated lean decls (4)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (4)
-
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 (4)
-
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 (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.
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
-
Missing tag metadata.
-
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 (1)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (3)
-
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.
Associated lean decls (4)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (1)
-
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 (2)
-
Missing tag metadata.
Associated lean decls (4)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
-
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 (2)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (4)
-
Missing tag metadata.
-
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 (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 (4)
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (4)
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (4)
-
Missing tag metadata.
-
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 (4)
-
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 (1)
-
Missing tag metadata.
Associated lean decls (5)
-
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 (3)
-
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 (3)
-
Missing tag metadata.
Associated lean decls (4)
-
Structure and coverage
Informal-only51Statements with no associated Lean code yet.
Ready to formalize9Entries with an actionable next formalization step.
Formalized, ancestors open253Local Lean work is done, but prerequisite closure is still open.
Fully closed102Local code and ancestor closure are both complete.
Blocked or incomplete42Entries not covered by the highlighted readiness buckets above.
Heaviest prerequisites (361)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 16statement deps: 16proof deps: 0direct uses: 2downstream unlocks: 4
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 15statement deps: 15proof deps: 0direct uses: 1downstream unlocks: 1
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 12statement deps: 12proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 11statement deps: 11proof deps: 0direct uses: 1downstream unlocks: 1
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 11statement deps: 11proof deps: 0direct uses: 1downstream unlocks: 1
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 10statement deps: 10proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 10statement deps: 10proof deps: 0direct uses: 5downstream unlocks: 7
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 10statement deps: 10proof deps: 0direct uses: 2downstream unlocks: 2
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 10statement deps: 10proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 10statement deps: 10proof deps: 0direct uses: 2downstream unlocks: 5
-
Show all 351 more heaviest-prerequisite entries
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 10statement deps: 10proof deps: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 9statement deps: 9proof deps: 0direct uses: 1downstream unlocks: 2
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 9statement deps: 9proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 9statement deps: 9proof deps: 0direct uses: 7downstream unlocks: 53
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 9statement deps: 9proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 9statement deps: 9proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 9statement deps: 9proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 8statement deps: 8proof deps: 0direct uses: 1downstream unlocks: 11
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 8statement deps: 8proof deps: 0direct uses: 1downstream unlocks: 18
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 8statement deps: 8proof deps: 0direct uses: 5downstream unlocks: 7
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 8statement deps: 8proof deps: 0direct uses: 8downstream unlocks: 18
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 8statement deps: 8proof deps: 0direct uses: 5downstream unlocks: 11
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 8statement deps: 8proof deps: 0direct uses: 3downstream unlocks: 3
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 8statement deps: 8proof deps: 0direct uses: 6downstream unlocks: 10
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 8statement deps: 8proof deps: 0direct uses: 7downstream unlocks: 7
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 8statement deps: 8proof deps: 0direct uses: 8downstream unlocks: 42
Associated lean decls (5)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 8statement deps: 8proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 8statement deps: 8proof deps: 0direct uses: 5downstream unlocks: 10
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 8statement deps: 8proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 8statement deps: 8proof deps: 0direct uses: 1downstream unlocks: 1
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 7statement deps: 7proof deps: 0direct uses: 16downstream unlocks: 67
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 7statement deps: 7proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 7statement deps: 7proof deps: 0direct uses: 1downstream unlocks: 3
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 7statement deps: 7proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 7statement deps: 7proof deps: 0direct uses: 1downstream unlocks: 1
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 7statement deps: 7proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 7statement deps: 7proof deps: 0direct uses: 2downstream unlocks: 5
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 7statement deps: 7proof deps: 0direct uses: 1downstream unlocks: 1
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 7statement deps: 7proof deps: 0direct uses: 6downstream unlocks: 13
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 7statement deps: 7proof deps: 0direct uses: 2downstream unlocks: 2
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 7statement deps: 7proof deps: 0direct uses: 4downstream unlocks: 15
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 7statement deps: 7proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 7statement deps: 7proof deps: 0direct uses: 5downstream unlocks: 8
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 7statement deps: 7proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 7statement deps: 7proof deps: 0direct uses: 4downstream unlocks: 6
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 6statement deps: 6proof deps: 0direct uses: 1downstream unlocks: 7
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 6statement deps: 6proof deps: 0direct uses: 2downstream unlocks: 2
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 6statement deps: 6proof deps: 0direct uses: 10downstream unlocks: 57
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 6statement deps: 6proof deps: 0direct uses: 1downstream unlocks: 1
Associated lean decls (5)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 6statement deps: 6proof deps: 0direct uses: 2downstream unlocks: 8
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 6statement deps: 6proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 6statement deps: 6proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 6statement deps: 6proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 6statement deps: 6proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 6statement deps: 6proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 6statement deps: 6proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 6statement deps: 6proof deps: 0direct uses: 3downstream unlocks: 8
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 6statement deps: 6proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 6statement deps: 6proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 6statement deps: 6proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 6statement deps: 6proof deps: 0direct uses: 1downstream unlocks: 1
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 6statement deps: 6proof deps: 0direct uses: 1downstream unlocks: 2
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 6statement deps: 6proof deps: 0direct uses: 1downstream unlocks: 2
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 6statement deps: 6proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 6statement deps: 6proof deps: 0direct uses: 4downstream unlocks: 27
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 6statement deps: 6proof deps: 0direct uses: 2downstream unlocks: 6
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 5proof deps: 0direct uses: 19downstream unlocks: 76
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 5proof deps: 0direct uses: 13downstream unlocks: 221
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 5proof deps: 0direct uses: 9downstream unlocks: 14
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 5proof deps: 0direct uses: 1downstream unlocks: 3
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 5proof deps: 0direct uses: 1downstream unlocks: 1
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 5proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 5proof deps: 0direct uses: 5downstream unlocks: 17
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 5proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 5proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 5proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 5proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 5proof deps: 0direct uses: 4downstream unlocks: 19
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 5proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 5proof deps: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 5proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 5proof deps: 0direct uses: 1downstream unlocks: 1
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 5proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 5proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 5proof deps: 0direct uses: 5downstream unlocks: 8
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 5proof deps: 0direct uses: 1downstream unlocks: 7
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 5proof deps: 0direct uses: 2downstream unlocks: 22
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 5proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 5proof deps: 0direct uses: 5downstream unlocks: 38
Associated lean decls (4)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 5proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 5proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 5proof deps: 0direct uses: 1downstream unlocks: 1
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 16downstream unlocks: 282
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 1downstream unlocks: 44
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 9downstream unlocks: 122
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 7downstream unlocks: 19
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 2downstream unlocks: 2
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 4downstream unlocks: 5
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 2downstream unlocks: 2
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 4downstream unlocks: 63
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct 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: 9downstream unlocks: 51
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 4downstream unlocks: 45
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 6downstream unlocks: 24
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 9downstream unlocks: 27
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 1downstream unlocks: 1
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 10downstream unlocks: 16
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 2downstream unlocks: 10
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 1downstream unlocks: 3
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 1downstream unlocks: 2
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: 9
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 2downstream unlocks: 13
Associated lean decls (4)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 7downstream unlocks: 211
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 2downstream unlocks: 20
Associated lean decls (4)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 4downstream unlocks: 30
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 3downstream unlocks: 30
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 83downstream unlocks: 113
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 12downstream unlocks: 26
Associated lean decls (5)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 2
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 20
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 19
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 4downstream unlocks: 6
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 5downstream unlocks: 22
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 3downstream unlocks: 23
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 3
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 13downstream unlocks: 24
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: 1
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 2downstream unlocks: 4
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 7downstream unlocks: 68
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 13downstream unlocks: 28
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (5)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 36downstream unlocks: 51
Associated lean decls (4)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 12
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 4downstream unlocks: 47
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 4downstream unlocks: 12
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: 16
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 11
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 4downstream unlocks: 12
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: 8
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 7downstream unlocks: 7
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 3downstream unlocks: 15
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: 1
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: 2
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 2downstream unlocks: 9
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 3downstream unlocks: 4
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 4downstream unlocks: 6
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 6
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 8
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 4downstream unlocks: 223
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: 11
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 (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 11
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 20
Associated lean decls (4)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 3downstream unlocks: 26
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: 21
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 19
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 5downstream unlocks: 11
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 8downstream unlocks: 24
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
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: 2
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 8downstream unlocks: 52
Associated lean decls (4)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 2downstream unlocks: 2
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: 1
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 5downstream unlocks: 40
Associated lean decls (4)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 4downstream unlocks: 36
Associated lean decls (5)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 2
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: 25
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 20downstream unlocks: 76
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 46
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 43
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 5downstream unlocks: 114
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: 32
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 12
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: 12
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 8
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream 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: 3downstream unlocks: 283
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 21
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 9
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 2
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 6downstream unlocks: 67
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: 2
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 11downstream unlocks: 59
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: 9
-
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: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
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: 6
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 29
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 20downstream unlocks: 66
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 30
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 8
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
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: 20
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 8downstream unlocks: 17
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 4downstream unlocks: 33
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream 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: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
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: 3
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream 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: 6downstream unlocks: 11
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: 10
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 5
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 8
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
-
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: 2downstream unlocks: 79
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 69
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 10
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: 2
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 5
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: 39
Associated lean decls (4)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream 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: 3downstream unlocks: 24
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 6
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 12
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 7downstream unlocks: 29
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 2
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 2
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
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: 29
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: 32
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 11downstream unlocks: 29
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 3
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream 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: 3downstream 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: 1downstream unlocks: 1
Associated lean decls (4)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
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
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
-
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 (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 15downstream unlocks: 95
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: 6
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (4)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
-
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 (4)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 9
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 16downstream unlocks: 184
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 33
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 5downstream unlocks: 153
Associated lean decls (5)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 6downstream unlocks: 37
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: 2downstream unlocks: 25
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: 2
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: 146
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: 31
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: 25
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 95downstream unlocks: 175
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: 123
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 116
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 5downstream unlocks: 116
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 6downstream unlocks: 51
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: 13
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 33
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: 1downstream unlocks: 123
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: 13
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 283
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: 224
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: 284
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 18
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 45
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 5downstream unlocks: 21
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: 16
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
-
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 (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: 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: 19
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: 5
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
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 28downstream unlocks: 70
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 5downstream 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: 2downstream unlocks: 2
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 13downstream unlocks: 56
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: 9
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 3
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 2
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 2
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 2
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 7downstream 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: 3
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 5downstream unlocks: 78
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: 64
Associated lean decls (4)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 5downstream unlocks: 41
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: 49
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: 14
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: 30
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: 10
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 65
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: 3
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: 1
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: 30
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: 2
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 80
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 15downstream unlocks: 193
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: 42
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 34
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 5downstream unlocks: 15
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: 2
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 46
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: 26
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 2
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: 25
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 3
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream 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: 3downstream unlocks: 100
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: 38
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: 2
Associated lean decls (4)
-
No prerequisites (45)
-
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 (3)
-
Show all 35 more entries without prerequisites
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (3)
-
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 (3)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (4)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (4)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
No dependents (106)
-
Associated lean decls (3)
-
Associated lean decls (4)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Show all 96 more entries without dependents
-
Associated lean decls (2)
-
Associated lean decls (3)
-
Associated lean decls (2)
-
Associated lean decls (5)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
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 (2)
-
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 (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (3)
-
Associated lean decls (1)