theorem proved term proof

`edges_QD`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  75theorem edges_QD (d : ℕ) : cube_edges d = d * 2 ^ (d - 1) := rfl

Term-mode proof.

  76
  77/-- Q₃ has exactly 12 undirected edges. -/

Lean names referenced from this declaration's body.