Theorem: div_rpow_neg_eq_rpow_div (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
x y s : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ x ^ (-s) / y ^ (-s) = (y / x) ^ s
Tactic:
rw [div_eq_mul_inv, Real.rpow_neg hx, Real.rpow_neg hy, Real.div_rpow hy hx]
State after:
x y s : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ (x ^ s)⁻¹ * (y ^ s)⁻¹⁻¹ = y ^ s / x ^ s

State before:
x y s : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ (x ^ s)⁻¹ * (y ^ s)⁻¹⁻¹ = y ^ s / x ^ s
Tactic:
field_simp
State after:
no goals