a little help with powers in lean

Stream: general

[מיכאל גרינבאום]

i am just starting to learn lean and i am trying to prove that for every complex number x, (x^3)^(1/3)=x, but without success and would like to get some help in proving it.
thanks in advance

[Johan Commelin]

@מיכאל גרינבאום Probably the statement isn't true...

[Johan Commelin]

The reason is that x ^ (1/3) will select a third root, but you don't know which one.

[Johan Commelin]

The other composition should work. So x ^ (1/3) ^ 3 = x

[מיכאל גרינבאום]

you are right, thanks,
how do you prove (x^(1/3))^3=x, and how to prove the previous statement if the field is R and not C?

[Kevin Buzzard]

For R the statement is not true in lean because the "function" which takes two reals x and y and returns x^y cannot be defined in any sensible way when x is negative in general, and so it returns junk results for all negative x; no attempt has been made to make it produce the mathematically sensible result in special cases such as y=1/3 where there happens to be a sensible answer.

[Kevin Buzzard]

For positive x the theorem is true and will follow easily from results in Lean's maths library. Rather than asking "how do I prove this in lean", the correct question is "how do I translate the following mathematical proof into lean". What is your mathematical proof of the theorem?

[Bryan Gin-ge Chen]

This thread might also be interesting to you: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Cube.20root.20of.20cubic.20is.20id.3F