Blueprint Summary
Overview
Total entries110completed: 110; deps incomplete: 0; sorries: 0; no proof: 0
Ready now0Entries with an actionable next formalization step.
Fully closed110Local code and prerequisite closure are both complete.
Actionable priorities0Entries ready now and already unlocking downstream work.
Entry index (110)
Definitions15completed: 15; deps incomplete: 0; sorries: 0; no proof: 0
Lemmas48completed: 48; deps incomplete: 0; sorries: 0; no proof: 0
Theorems47completed: 47; deps incomplete: 0; sorries: 0; no proof: 0
Definition Index (15)
-
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)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
Theorem / Proposition / Lemma / Corollary Index (95)
-
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)
-
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)
-
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)
-
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)
-
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)
-
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)
-
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)
-
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)
By parent groups (7)
Infinitude of primes. (26)
-
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)
-
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)
-
Associated lean decls (1)
-
Associated lean decls (1)
Fermat's Little Theorem. (8)
-
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)
Wagon's theorem on tiling a rectangle by rectangles with an integer side. (41)
-
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)
-
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)
-
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)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
Irrationality of square root of 2. (4)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
Combinatorial identities. (4)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
Fermat's theorem on sums of two squares. (5)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
Basel problem. (7)
-
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)
Dependency insights
Statement-used entries16Entries reused in statement dependencies.
Proof-used entries52Entries reused in proof-only dependencies.
Tracked parent groups7Grouped health rollups for parents with more than one child entry.
Most used in statements (16)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 6
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 1direct uses: 3downstream unlocks: 3
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 3
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 3
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 4
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 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 (1)
-
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 (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
Associated lean decls (1)
-
Show all 6 more statement-used entries
-
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: 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: 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
Associated lean decls (1)
-
Most used in proofs (52)
-
Reverse dependencies recorded in proof dependencies.proof uses: 5statement uses: 0direct uses: 5downstream unlocks: 14
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 3statement uses: 0direct uses: 3downstream unlocks: 3
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 4
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 3
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 3
Associated lean decls (1)
-
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: 2statement uses: 0direct uses: 2downstream 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: 2statement uses: 0direct uses: 2downstream unlocks: 2
Associated lean decls (1)
-
Show all 42 more proof-used entries
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 5
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 4
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 4
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 2direct uses: 3downstream unlocks: 3
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 3
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 3
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 3
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 3
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Group health (7)
-
Wagon's theorem on tiling a rectangle by rectangles with an integer side.Grouped view over entries sharing the same parent.total: 42closed: 42local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 67Next: no ready child currently unlocks downstream work.
-
Infinitude of primes.Grouped view over entries sharing the same parent.total: 30closed: 30local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 35Next: no ready child currently unlocks downstream work.
-
Fermat's Little Theorem.Grouped view over entries sharing the same parent.total: 11closed: 11local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 14Next: no ready child currently unlocks downstream work.
-
Basel problem.Grouped view over entries sharing the same parent.total: 9closed: 9local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 13Next: no ready child currently unlocks downstream work.
-
Irrationality of square root of 2.Grouped view over entries sharing the same parent.total: 6closed: 6local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 9Next: no ready child currently unlocks downstream work.
-
Fermat's theorem on sums of two squares.Grouped view over entries sharing the same parent.total: 6closed: 6local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 2Next: no ready child currently unlocks downstream work.
-
Combinatorial identities.Grouped view over entries sharing the same parent.total: 6closed: 6local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0Next: no ready child currently unlocks downstream work.
Metadata
Metadata audit
Missing owner110
Missing effort110
Untagged110
Missing owner (110)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Show all 100 more entries missing owner
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
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 effort (110)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Show all 100 more entries missing effort
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
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)
-
Untagged (110)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Show all 100 more untagged entries
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
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)
-
Structure and coverage
Fully closed110Local code and ancestor closure are both complete.
Heaviest prerequisites (62)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 0proof deps: 4direct 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: 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
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
Associated lean decls (1)
-
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: 2statement deps: 0proof deps: 2direct uses: 1downstream unlocks: 2
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: 2
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 0proof 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: 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: 0downstream unlocks: 0
Associated lean decls (1)
-
Show all 52 more heaviest-prerequisite entries
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 0proof 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: 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: 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: 2
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: 3downstream 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: 2downstream 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: 1downstream unlocks: 1
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: 1
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: 1
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
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: 5
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
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: 1
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: 4
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: 1
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: 1
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: 1
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: 1
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: 3
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: 2
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: 1
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
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: 1
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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: 3
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
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 (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 (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)
-
No prerequisites (48)
-
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)
-
Show all 38 more entries without prerequisites
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (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)
-
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)
-
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)
-
No dependents (45)
-
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)
-
Show all 35 more entries without dependents
-
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)
-
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)
-
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)
-