def definition def or abbrev

`F`

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

formal statement (Lean)

  89def F₂ (D : ℕ) : ℕ := (D * (D - 1) / 2) * 2 ^ (D - 2)

Definition body.

  90
  91/-- Face pairs: opposite faces sharing a normal axis. For the D-cube,
  92    the number of 2-face pair axes equals C(D,2). -/