pith. machine review for the scientific record. sign in
def definition def or abbrev

window8Sum

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)

  75def window8Sum (f : ℕ → ℝ) (Z0 : ℕ) : ℝ :=

proof body

Definition body.

  76  (Finset.range 8).sum (fun k => f (Z0 + k))
  77
  78/-! ## Noble Gas Closure Infrastructure
  79
  80We define a valence proxy and prove that noble gases are exactly the
  818-window closure points.
  82-/
  83
  84/-- The canonical noble gas atomic numbers (first 6 periods + Oganesson). -/

used by (2)

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

depends on (5)

Lean names referenced from this declaration's body.