Incomplete assumption in Section 5 Epilogue?

[daikonradish]

analysis/Analysis/Section_5_epilogue.lean

Line 249 in cd83236

theorem Real.ratPow_of_equivR (x:Real) (q:ℚ) : equivR (x^q) = (equivR x)^(q:ℝ) := by

Hi, I think the assumption list here is incomplete. I've been looking at this for some time and I feel that another assumption is required in order to rewrite the lemmas from this section: (hx : x > 0). Otherwise, it's not possible to rewrite using Section 5.6's Real.ratPow_def.

[rkirov]

That is true, I have added that extra assumption in my solutions but forgot to upstream them - https://github.com/rkirov/analysis/blob/main/Analysis/Section_5_epilogue.lean#L841 . I recommend you open a PR