Theorem: div_rpow_eq_rpow_neg (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
a x s : ℝ
hx : 0 ≤ x
⊢ a / x ^ s = a * x ^ (-s)
Tactic:
rw [div_eq_mul_inv, Real.rpow_neg hx]
State after:
no goals