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

gap_zero

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)

  29@[simp] theorem gap_zero : gap (0 : ℤ) = 0 := by

proof body

Term-mode proof.

  30  simp [gap]
  31
  32/-!
  33`gap` can be rewritten as a shifted log-base-φ:
  34
  35  `gap(Z) = log_φ(φ + Z) - 1`
  36
  37for any `Z` with `0 < φ + Z` (in practice all `Z ≥ 0` used in the mass bands).
  38-/

used by (1)

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

depends on (12)

Lean names referenced from this declaration's body.