Blueprint Summary
Overview
Total entries209completed: 53; deps incomplete: 54; sorries: 0; no proof: 66
Ready now2Entries whose next formalization step is currently unblocked.
Fully closed53Local code and prerequisite closure are both complete.
Actionable priorities40Entries ready now and already unlocking downstream work.
Current blockers3Missing external or incomplete Lean declarations.
Ready next (40)
-
Ready for proof work.stage: proofstatement: ready to formalizedirect uses: 2downstream unlocks: 61proof: ready to formalize
-
Ready for proof work.stage: proofstatement: ready to formalizedirect uses: 2downstream unlocks: 45proof: ready to formalize
-
Ready for proof work.stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 44proof: ready to formalize
-
Ready for proof work.stage: proofstatement: ready to formalizedirect uses: 2downstream unlocks: 35proof: ready to formalize
-
Ready for statement work.stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 24
-
Ready for statement work.stage: statementstatement: ready to formalizedirect uses: 2downstream unlocks: 14
-
Ready for statement work.stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 14
-
Ready for proof work.stage: proofstatement: ready to formalizedirect uses: 2downstream unlocks: 13proof: ready to formalize
-
Ready for proof work.stage: proofstatement: ready to formalizedirect uses: 2downstream unlocks: 13proof: ready to formalize
-
Ready for statement work.stage: statementstatement: ready to formalizedirect uses: 8downstream unlocks: 12
-
Show all 30 more priorities
-
Ready for statement work.stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 12
-
Ready for statement work.stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 12
-
Ready for proof work.stage: proofstatement: ready to formalizedirect uses: 3downstream unlocks: 11proof: ready to formalize
-
Ready for proof work.stage: proofstatement: ready to formalizedirect uses: 2downstream unlocks: 11proof: ready to formalize
-
Ready for proof work.stage: proofstatement: ready to formalizedirect uses: 2downstream unlocks: 11proof: ready to formalize
-
Ready for proof work.stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 11proof: ready to formalize
-
Ready for proof work.stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 11proof: ready to formalize
-
Ready for proof work.stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 11proof: ready to formalize
-
Ready for proof work.stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 10proof: ready to formalize
-
Ready for statement work.stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 10
-
Ready for statement work.stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 9
-
Ready for statement work.stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 8
-
Ready for statement work.stage: statementstatement: ready to formalizedirect uses: 2downstream unlocks: 6
-
Ready for proof work.stage: proofstatement: ready to formalizedirect uses: 3downstream unlocks: 5proof: ready to formalize
-
Ready for statement work.stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 5
-
Ready for proof work.stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 4proof: ready to formalize
-
Ready for statement work.stage: statementstatement: ready to formalizedirect uses: 2downstream unlocks: 3
-
Ready for statement work.stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 3proof: not ready
-
Ready for proof work.stage: proofstatement: ready to formalizedirect uses: 2downstream unlocks: 2proof: ready to formalize
-
Ready for proof work.stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 2proof: ready to formalize
-
Ready for proof work.stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 2proof: ready to formalize
-
Ready for statement work.stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 2proof: not ready
-
Ready for proof work.stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 1proof: ready to formalize
-
Ready for statement work.stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 1
-
Ready for statement work.stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 1
-
Ready for statement work.stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 1proof: not ready
-
Ready for statement work.stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 1
-
Ready for statement work.stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Ready for statement work.stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 1
-
Ready for statement work.stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 1
-
Current blockers (3)
-
Missing external Lean declaration:
NormedSpace.Dual[missing declaration] -
Missing external Lean declaration:
NumberField.tendsto_sub_one_mul_dedekindZeta_nhdsGT[missing declaration] -
Missing external Lean declaration:
NumberField.dedekindZeta[missing declaration]
Entry index (209)
Definitions73completed: 25; deps incomplete: 13; sorries: 0; no proof: 0
Propositions36completed: 7; deps incomplete: 10; sorries: 0; no proof: 19
Lemmas48completed: 17; deps incomplete: 11; sorries: 0; no proof: 20
Theorems41completed: 3; deps incomplete: 16; sorries: 0; no proof: 21
Corollaries11completed: 1; deps incomplete: 4; sorries: 0; no proof: 6
Informal-only entries99
Definition Index (73)
-
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 (2)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (4)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (5)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (3)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
Theorem / Proposition / Lemma / Corollary Index (136)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (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 (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (4)
-
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 (2)
-
Associated lean decls (3)
-
Associated lean decls (1)
Dependency insights
Statement-used entries123Entries reused in statement dependencies.
Proof-used entries107Entries reused in proof-only dependencies.
Most used in statements (123)
-
Reverse dependencies recorded in statement dependencies.statement uses: 12proof uses: 6direct uses: 18downstream unlocks: 35
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 10proof uses: 3direct uses: 13downstream unlocks: 76
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 10proof uses: 1direct uses: 11downstream unlocks: 37
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 9proof uses: 0direct uses: 9downstream unlocks: 59
-
Reverse dependencies recorded in statement dependencies.statement uses: 9proof uses: 3direct uses: 12downstream unlocks: 28
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 7proof uses: 1direct uses: 8downstream unlocks: 25
-
Reverse dependencies recorded in statement dependencies.statement uses: 7proof uses: 1direct uses: 8downstream unlocks: 12
-
Reverse dependencies recorded in statement dependencies.statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 92
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 5proof uses: 1direct uses: 6downstream unlocks: 43
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 5proof uses: 2direct uses: 7downstream unlocks: 42
Associated lean decls (1)
-
Show all 113 more statement-used entries
-
Reverse dependencies recorded in statement dependencies.statement uses: 5proof uses: 4direct uses: 9downstream unlocks: 25
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 3direct uses: 7downstream unlocks: 17
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 13
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 11
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 1direct uses: 5downstream unlocks: 8
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 8
Associated lean decls (4)
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 1direct uses: 5downstream unlocks: 7
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 79
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 38
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 2direct uses: 5downstream unlocks: 12
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 1direct uses: 4downstream unlocks: 7
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 2direct uses: 5downstream unlocks: 4
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 1direct uses: 4downstream unlocks: 3
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 1direct uses: 3downstream unlocks: 89
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 1direct uses: 3downstream unlocks: 62
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 60
-
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: 45
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 1direct uses: 3downstream unlocks: 35
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 1direct uses: 3downstream unlocks: 35
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 1direct uses: 3downstream unlocks: 34
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 2direct uses: 4downstream unlocks: 32
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 4direct uses: 6downstream unlocks: 23
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 14
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 2direct uses: 4downstream unlocks: 13
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 3direct uses: 5downstream unlocks: 12
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 11
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 2direct uses: 4downstream unlocks: 9
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 1direct uses: 3downstream unlocks: 8
Associated lean decls (1)
-
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: 1direct uses: 3downstream unlocks: 5
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 1direct uses: 3downstream unlocks: 4
Associated lean decls (1)
-
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: 2direct uses: 4downstream unlocks: 3
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 2direct uses: 4downstream 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: 2direct uses: 4downstream 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: 1proof uses: 0direct uses: 1downstream unlocks: 94
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 93
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 61
-
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: 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: 1direct uses: 2downstream unlocks: 38
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 37
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 35
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 24
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 24
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 23
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 3direct uses: 4downstream unlocks: 19
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 14
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 13
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 13
-
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: 2direct uses: 3downstream unlocks: 11
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 11
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 11
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 11
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 10
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 10
-
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
Associated lean decls (2)
-
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: 1direct uses: 2downstream unlocks: 8
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 8
-
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: 1direct uses: 2downstream unlocks: 7
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 7
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 6
Associated lean decls (2)
-
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: 1direct uses: 2downstream unlocks: 5
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 5
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 5
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 5
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 5
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 5
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 5
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 4
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
Associated lean decls (5)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 1direct uses: 2downstream 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
-
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 (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 2direct uses: 3downstream unlocks: 2
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 2
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 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
Associated lean decls (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: 1direct uses: 2downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 1
Associated lean decls (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
-
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
-
Most used in proofs (107)
-
Reverse dependencies recorded in proof dependencies.proof uses: 6statement uses: 12direct uses: 18downstream unlocks: 35
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 4statement uses: 5direct uses: 9downstream unlocks: 25
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 4statement uses: 0direct uses: 4downstream unlocks: 25
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 4statement uses: 2direct uses: 6downstream unlocks: 23
-
Reverse dependencies recorded in proof dependencies.proof uses: 3statement uses: 10direct uses: 13downstream unlocks: 76
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 3statement uses: 9direct uses: 12downstream unlocks: 28
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 3statement uses: 1direct uses: 4downstream unlocks: 19
-
Reverse dependencies recorded in proof dependencies.proof uses: 3statement uses: 4direct uses: 7downstream unlocks: 17
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 3statement uses: 0direct uses: 3downstream unlocks: 13
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 3statement uses: 2direct uses: 5downstream unlocks: 12
-
Show all 97 more proof-used entries
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 5direct uses: 7downstream unlocks: 42
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 2direct uses: 4downstream unlocks: 32
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 25
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 20
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 2direct uses: 4downstream unlocks: 13
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 3direct uses: 5downstream unlocks: 12
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 12
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 1direct uses: 3downstream unlocks: 11
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 11
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 10
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 2direct uses: 4downstream unlocks: 9
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 9
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 3direct uses: 5downstream unlocks: 4
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 2direct uses: 4downstream unlocks: 3
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 2direct uses: 4downstream unlocks: 3
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 3
Associated lean decls (3)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 2direct uses: 4downstream unlocks: 2
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 1direct uses: 3downstream unlocks: 2
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 2
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 2direct uses: 3downstream unlocks: 89
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 2direct uses: 3downstream unlocks: 62
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 61
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 5direct uses: 6downstream unlocks: 43
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 40
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 40
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 39
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 39
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 38
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 10direct uses: 11downstream unlocks: 37
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 37
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 2direct uses: 3downstream unlocks: 35
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 2direct uses: 3downstream unlocks: 35
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 35
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 2direct uses: 3downstream unlocks: 34
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 26
Associated lean decls (3)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 7direct uses: 8downstream unlocks: 25
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 24
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 24
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 23
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 23
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 23
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 13
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 13
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 7direct uses: 8downstream unlocks: 12
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 12
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 11
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 11
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 11
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 11
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 11
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 11
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 11
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 11
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 10
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 10
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 10
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 10
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 9
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 4direct uses: 5downstream unlocks: 8
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 2direct uses: 3downstream unlocks: 8
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 8
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 8
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 4direct uses: 5downstream unlocks: 7
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 3direct uses: 4downstream unlocks: 7
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 7
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 7
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 7
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 2direct uses: 3downstream unlocks: 5
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 5
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 5
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 5
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 5
Associated lean decls (3)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 2direct uses: 3downstream unlocks: 4
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 4
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 4
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 3direct uses: 4downstream unlocks: 3
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 3
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 3
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 3
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 2
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 2
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (3)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Metadata
Metadata audit
Missing owner209
Missing effort209
Untagged209
Missing owner (209)
-
Missing owner metadata.
-
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.
Associated lean decls (2)
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Show all 199 more entries missing owner
-
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 (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.
-
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 (3)
-
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.
-
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.
-
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.
Associated lean decls (2)
-
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 (1)
-
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 (2)
-
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 (1)
-
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 (2)
-
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.
Associated lean decls (1)
-
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.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
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.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
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 (2)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
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 (5)
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
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 (4)
-
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.
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (4)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
-
Missing effort (209)
-
Missing effort metadata.
-
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.
Associated lean decls (2)
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Show all 199 more entries missing effort
-
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 (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.
-
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 (3)
-
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.
-
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.
-
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.
Associated lean decls (2)
-
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 (1)
-
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 (2)
-
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 (1)
-
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 (2)
-
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.
Associated lean decls (1)
-
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.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
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.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
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 (2)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
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 (5)
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
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 (4)
-
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.
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (4)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
-
Untagged (209)
-
Missing tag metadata.
-
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.
Associated lean decls (2)
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
-
Show all 199 more untagged entries
-
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 (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.
-
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 (3)
-
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.
-
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.
-
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.
Associated lean decls (2)
-
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 (1)
-
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 (2)
-
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 (1)
-
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 (2)
-
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.
Associated lean decls (1)
-
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.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
-
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.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
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 (2)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
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 (5)
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
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 (4)
-
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.
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (4)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
-
Structure and coverage
Informal-only99Statements with no associated Lean code yet.
Ready to formalize2Entries whose next step is currently unblocked.
Formalized, ancestors open54Local Lean work is done, but prerequisite closure is still open.
Fully closed53Local code and ancestor closure are both complete.
Blocked or incomplete1Entries not covered by the highlighted readiness buckets above.
Heaviest prerequisites (145)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 8statement deps: 0proof deps: 8direct uses: 1downstream unlocks: 1
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 7statement deps: 3proof deps: 5direct uses: 3downstream unlocks: 8
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 6statement deps: 0proof deps: 6direct uses: 2downstream unlocks: 9
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 6statement deps: 5proof deps: 5direct uses: 1downstream unlocks: 9
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 6statement deps: 4proof deps: 3direct 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: 3
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 0proof deps: 5direct uses: 1downstream unlocks: 10
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 4proof deps: 4direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 3proof deps: 4direct uses: 1downstream unlocks: 3
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 1proof deps: 4direct uses: 0downstream unlocks: 0
Associated lean decls (2)
-
Show all 135 more heaviest-prerequisite entries
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 5proof deps: 3direct uses: 0downstream unlocks: 0
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 4proof deps: 1direct uses: 5downstream unlocks: 7
-
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: 1downstream unlocks: 4
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 5proof deps: 0direct uses: 1downstream unlocks: 3
-
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: 4statement deps: 0proof deps: 4direct uses: 1downstream unlocks: 23
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 0proof deps: 4direct uses: 1downstream unlocks: 23
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 0proof deps: 4direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 0proof deps: 4direct uses: 1downstream unlocks: 39
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 3direct uses: 1downstream unlocks: 7
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 2direct uses: 8downstream unlocks: 25
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 3proof deps: 2direct uses: 3downstream unlocks: 4
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 2proof deps: 2direct uses: 6downstream unlocks: 23
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 2proof deps: 2direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 1direct uses: 3downstream unlocks: 34
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 7downstream unlocks: 17
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: 5
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 2downstream unlocks: 4
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 3direct uses: 0downstream unlocks: 0
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 0proof deps: 3direct uses: 1downstream unlocks: 11
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 0proof deps: 3direct uses: 1downstream unlocks: 1
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 0proof deps: 3direct uses: 2downstream unlocks: 1
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 0proof deps: 3direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 2direct uses: 2downstream unlocks: 3
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 1proof deps: 2direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 1proof deps: 2direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 1direct uses: 1downstream unlocks: 1
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 1direct uses: 2downstream unlocks: 7
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 1direct 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: 1direct uses: 2downstream unlocks: 5
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 1direct uses: 4downstream unlocks: 3
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 4downstream unlocks: 9
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 18downstream unlocks: 35
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 13downstream unlocks: 76
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: 2
-
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: 2downstream unlocks: 2
-
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: 4downstream unlocks: 3
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 6downstream unlocks: 43
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 2direct uses: 5downstream unlocks: 4
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 2direct uses: 2downstream unlocks: 60
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 2direct uses: 2downstream unlocks: 10
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 2direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 2direct uses: 1downstream unlocks: 3
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 2direct uses: 1downstream unlocks: 10
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 1proof deps: 2direct uses: 0downstream unlocks: 0
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 0proof deps: 2direct uses: 1downstream unlocks: 23
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 0proof deps: 2direct uses: 2downstream unlocks: 20
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 0proof deps: 2direct uses: 2downstream unlocks: 10
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 0proof deps: 2direct uses: 1downstream unlocks: 11
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 0proof deps: 2direct uses: 2downstream unlocks: 38
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 1direct uses: 2downstream unlocks: 7
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 1direct uses: 4downstream unlocks: 2
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 1direct uses: 1downstream unlocks: 40
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 1direct uses: 1downstream unlocks: 1
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 1proof deps: 1direct uses: 1downstream unlocks: 2
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 1proof deps: 1direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 1proof deps: 1direct uses: 2downstream unlocks: 8
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 1proof deps: 1direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 1proof deps: 1direct uses: 2downstream unlocks: 3
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 1proof deps: 1direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 1proof deps: 1direct uses: 0downstream unlocks: 0
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 1proof deps: 1direct uses: 0downstream unlocks: 0
-
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: 1downstream unlocks: 1
-
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: 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: 2
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 4downstream unlocks: 32
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 5downstream unlocks: 8
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 4downstream unlocks: 3
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: 37
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: 2downstream unlocks: 11
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 4downstream unlocks: 13
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 35
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
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: 1
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 4
Associated lean decls (5)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 7downstream unlocks: 42
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 3
-
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: 4
-
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: 44
-
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: 12downstream unlocks: 28
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: 5
-
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 (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 1direct uses: 5downstream unlocks: 12
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 1direct uses: 5downstream unlocks: 12
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 1direct uses: 2downstream unlocks: 11
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 0proof deps: 1direct uses: 2downstream unlocks: 25
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 0proof deps: 1direct uses: 4downstream unlocks: 19
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 0proof deps: 1direct uses: 1downstream unlocks: 3
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 0proof deps: 1direct uses: 1downstream unlocks: 11
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 0proof deps: 1direct uses: 1downstream unlocks: 2
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 0proof deps: 1direct uses: 1downstream unlocks: 11
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 0proof deps: 1direct uses: 1downstream unlocks: 10
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 0proof deps: 1direct uses: 3downstream unlocks: 2
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 0proof deps: 1direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 0proof deps: 1direct uses: 1downstream unlocks: 2
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 0proof deps: 1direct 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: 23
-
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: 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: 1
-
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: 11
-
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: 35
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 5
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 9downstream unlocks: 59
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 93
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: 89
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: 61
-
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: 1downstream unlocks: 1
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 62
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: 1
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 6
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 (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 5
Associated lean decls (3)
-
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 (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 5downstream unlocks: 92
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: 8
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: 2
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 (4)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 9
-
No prerequisites (64)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Show all 54 more entries without prerequisites
-
Associated lean decls (1)
-
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 (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (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)
No dependents (40)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Show all 30 more entries without dependents
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (4)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-