lemma proved term proof

`PhiPow_neg`

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

formal statement (Lean)

  83@[simp] lemma PhiPow_neg (y : ℝ) : PhiPow (-y) = 1 / PhiPow y := by

Term-mode proof.

  84  have := PhiPow_sub 0 y
  85  simp [PhiPow_zero, sub_eq_add_neg] at this
  86  simpa using this
  87

Lean names referenced from this declaration's body.