Re: [isabelle] ln on negative numbers

Yes, I meant for all non-zero real x, of course. That would be quite

On 30/04/15 16:11, Larry Paulson wrote:
> This identity holds for the real parts. For the imaginary parts, there is potentially a difference of 2*pi*i due to the branch cut.
> Larry Paulson
>> On 30 Apr 2015, at 11:05, Manuel Eberl <eberlm at> wrote:
>> As long as "(a*b) powr c = a powr c * b powr c" holds unconditionally, I am happy. And if I am not mistaken, that is the case iff "ln (a*b) = ln a + ln b" holds for all non-zero a,b.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.