theorem proved wrapper

`peakFrequency_succ`

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

formal statement (Lean)

  45theorem peakFrequency_succ (k : ℕ) :
  46    peakFrequency (k + 1) = peakFrequency k * phi := by

One-line wrapper that applies unfold.

  47  unfold peakFrequency; rw [pow_succ]; ring
  48

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

adjacent_class_ratio in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
asteroidOreSpectroscopyCert in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
ore_spectroscopy_one_statement in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use

Lean names referenced from this declaration's body.

peakFrequency in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use