No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
29def spanAt (d : ℕ) : ℕ := 2 ^ d - 1
proof body
Definition body.
30
used by (8)
From the project-wide theorem graph. These declarations reference this one in their body.
-
span_at_0
in IndisputableMonolith.CrossDomain.WorkingMemoryFromCube
decl_use
-
span_at_1
in IndisputableMonolith.CrossDomain.WorkingMemoryFromCube
decl_use
-
span_at_2
in IndisputableMonolith.CrossDomain.WorkingMemoryFromCube
decl_use
-
span_at_3
in IndisputableMonolith.CrossDomain.WorkingMemoryFromCube
decl_use
-
span_at_4
in IndisputableMonolith.CrossDomain.WorkingMemoryFromCube
decl_use
-
span_strict_mono
in IndisputableMonolith.CrossDomain.WorkingMemoryFromCube
decl_use
-
super_normal_jump
in IndisputableMonolith.CrossDomain.WorkingMemoryFromCube
decl_use
-
WorkingMemoryFromCubeCert
in IndisputableMonolith.CrossDomain.WorkingMemoryFromCube
decl_use