Theorem: Real.inv_rpow' (PrimeNumberTheoremAnd/Tactic/RPowSimp.lean)

State before:
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ x⁻¹ ^ y = x ^ (-y)
Tactic:
simp only [← rpow_neg_one, ← rpow_mul hx, neg_mul, one_mul]
State after:
no goals