Re: [isabelle] ln on negative numbers



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

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 in.tum.de> 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.