pith. machine review for the scientific record. sign in
theorem proved term proof

Q3_euler_characteristic

show as:
view Lean formalization →

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)

 109theorem Q3_euler_characteristic : V 3 + F₂ 3 = E 3 + 2 := by native_decide

proof body

Term-mode proof.

 110
 111/-- The Q₃ cube is self-dual: the number of vertices equals the number
 112    of 3-cells (just 1 cube), and vertices = 2^D while the dual has
 113    the same combinatorics. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (17)

Lean names referenced from this declaration's body.