lemma proved term proof

`PhiPow_one`

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

formal statement (Lean)

  78@[simp] lemma PhiPow_one : PhiPow 1 = Constants.phi := by

Term-mode proof.

  79  unfold PhiPow
  80  have hφ : 0 < Constants.phi := Constants.phi_pos
  81  simp [one_mul, Real.exp_log hφ]
  82

Lean names referenced from this declaration's body.