Theorem: Real.pow_neg (PrimeNumberTheoremAnd/Tactic/RPowSimp.lean)

State before:
a b : ℝ
h : 0 ≤ a
⊢ a ^ (-b) = a⁻¹ ^ b
Tactic:
simp [← rpow_neg_one, ← rpow_mul h]
State after:
no goals