How to prove this equation(x>0, Odd n, (-x)^(1/n)=-x^(1/n))?

Stream: Analysis I

[Tang zhengyang]

I am trying to prove this seemingly simple proposition:

lemma ex2 (x : ℝ) (hx: x > 0): (-x) ^ (1 / 5 : ℝ) = -x ^ (1 / 5 : ℝ) := by sorry

I searched for a long time using Leansearch and found that there seem to be no tactics that can directly handle cases like this “(-x) ^ (1 / n)， Odd n” :

example (x : ℝ)(nodd: Odd n)(hx: x > 0): (-x) ^ (1 / n : ℝ) = -x ^ (1 / n : ℝ) := by sorry

Most tactics for dealing with exponents require that ```

(-x) ≥ 0

This problem has been bothering me for a long time. Even though it seems very simple, I wonder if I have missed some tactics. Otherwise, how can it be proven? Thank you.

[Aaron Liu]

I don't think this one is true

[Aaron Liu]

beware of the junk values

import Mathlib

example (x : ℝ) (hx : 0 < x) : (-x) ^ (1 / 5 : ℝ) = x ^ (1 / 5 : ℝ) * Real.cos (Real.pi / 5) := by
  rw [Real.rpow_def_of_neg (neg_lt_zero.2 hx), Real.rpow_def_of_pos hx,
    Real.log_neg_eq_log, one_div_mul_eq_div]

[Kenny Lau]

@Tang zhengyang think about how exponent would need to be defined for your proposition to be true

[Kenny Lau]

given (-2)^r, the definition would need to check if the real number(!) r is of the form p/q with p odd integer and q even integer p integer and q odd integer

[Kenny Lau]

which, you know, i guess is possible

[Alex Meiburg]

Yeah, there are people talking about changing Mathlib's definition to do something like that :)

[Kenny Lau]

where's the thread?