pith. machine review for the scientific record. sign in
theorem proved wrapper

uniform_ratio

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)

  73theorem uniform_ratio (L : ZeroParameterLedger) :
  74    ∀ n, L.levels n / L.levels (n + 1) = L.levels 0 / L.levels 1 :=

proof body

One-line wrapper that applies L.no_external_scale.

  75  L.no_external_scale 1 one_pos
  76

used by (3)

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

depends on (3)

Lean names referenced from this declaration's body.