Theorem: div_cpow_eq_cpow_neg (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
a x s : ℂ
⊢ a / x ^ s = a * x ^ (-s)
Tactic:
rw [div_eq_mul_inv, cpow_neg]
State after:
no goals