theorem proved wrapper

`phi_power_ratio`

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

formal statement (Lean)

 275theorem phi_power_ratio (a b : ℤ) :
 276    PhiForcing.φ ^ a / PhiForcing.φ ^ b = PhiForcing.φ ^ (a - b) := by

One-line wrapper that applies rw.

 277  rw [div_eq_mul_inv, ← zpow_neg, ← zpow_add₀ PhiForcing.phi_pos.ne', sub_eq_add_neg]
 278