Theorem: one_div_cpow_eq_cpow_neg (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
x s : ℂ
⊢ 1 / x ^ s = x ^ (-s)
Tactic:
convert div_cpow_eq_cpow_neg 1 x s using 1
State after:
case h.e'_3
x s : ℂ
⊢ x ^ (-s) = 1 * x ^ (-s)

State before:
case h.e'_3
x s : ℂ
⊢ x ^ (-s) = 1 * x ^ (-s)
Tactic:
simp
State after:
no goals