Re: [isabelle] ln on negative numbers



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.