pith. machine review for the scientific record. sign in
lemma proved tactic proof

PhiPow_add

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)

  49lemma PhiPow_add (x y : ℝ) : PhiPow (x + y) = PhiPow x * PhiPow y := by

proof body

Tactic-mode proof.

  50  unfold PhiPow
  51  have hx : Real.log (Constants.phi) * (x + y)
  52        = Real.log (Constants.phi) * x + Real.log (Constants.phi) * y := by
  53    ring
  54  simp [hx, Real.exp_add]
  55

depends on (2)

Lean names referenced from this declaration's body.