Theorem: ipow_mul_inv_eq_one (HOLFloat/Common.lean)

State before:
r : ℝ
i : ℤ
⊢ 0 < r → r ^ i * r ^ (-i) = 1
Tactic:
sorry
State after:
no goals