Theorem: ipow_add_exp (HOLFloat/Common.lean)

State before:
r : ℝ
u v : ℤ
⊢ r ≠ 0 → r ^ u * r ^ v = r ^ (u + v)
Tactic:
sorry
State after:
no goals