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

ZeroParameterLedger

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)

  33structure ZeroParameterLedger where
  34  levels : ℕ → ℝ
  35  all_positive : ∀ n, 0 < levels n
  36  no_external_scale : ∀ (λ : ℝ), λ > 0 →
  37    ∀ n, levels n / levels (n + 1) = levels 0 / levels 1
  38

used by (7)

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