metamath / set.mm

Metamath source file for logic and set theory
Other
246 stars 88 forks source link

intuitionize ^c from df-cxp to cxplea #4047

Closed jkingdon closed 3 months ago

jkingdon commented 3 months ago

Taking a closer look at this topic, for example https://en.wikipedia.org/wiki/Exponentiation#Complex_exponentiation , shows that a complex number to a complex power has the same kinds of issues that we see for complex square root and others, in terms of choosing which branch to follow.

However, everything goes quite smoothly if we consider a positive real to a complex power, which is what fits naturally with our definition of logarithm and theorems for logarithms. That is the path taken here.

This is a long section so this pull request is the first part of it.