Theorem: ipow_to_one (HOLFloat/Common.lean)

State before:
r : ℝ
⊢ r ^ 1 = r
Tactic:
simp
State after:
no goals