def definition def or abbrev

`neutral8`

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

formal statement (Lean)

  31def neutral8 (w : ℕ → ℝ) (i0 : ℕ) : ℝ :=

Definition body.

  32  (Finset.range 8).sum (fun i => w (i0 + i))
  33
  34/‑ Count legal triads in a finite list. -/

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

Lean names referenced from this declaration's body.