Theorem: Complex.cpow_neg_eq_inv_pow_ofReal_pos (PrimeNumberTheoremAnd/PerronFormula.lean)

State before:
a : ℝ
ha : 0 < a
r : ℂ
⊢ ↑a ^ (-r) = (↑a)⁻¹ ^ r
Tactic:
rw [cpow_neg, ← Complex.inv_cpow]
State after:
case hx
a : ℝ
ha : 0 < a
r : ℂ
⊢ (↑a).arg ≠ π

State before:
case hx
a : ℝ
ha : 0 < a
r : ℂ
⊢ (↑a).arg ≠ π
Tactic:
exact slitPlane_arg_ne_pi (Or.inl ha)
State after:
no goals