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

State before:
x : ℝ
hx : 0 < x
y : ℂ
⊢ ↑x ^ y = cexp (↑x.log * y)
Tactic:
simp [← Complex.cpow_eq_pow, Complex.cpow, hx.ne.symm, ← Complex.ofReal_log hx.le]
State after:
no goals