*To*: Manuel Eberl <eberlm at in.tum.de>*Subject*: Re: [isabelle] ln on negative numbers*From*: Larry Paulson <lp15 at cam.ac.uk>*Date*: Thu, 30 Apr 2015 15:11:06 +0100*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <5541FE85.3050707@in.tum.de>*References*: <5540E488.6070106@in.tum.de> <7280EAEA-8715-472E-8B9E-6C11AC41F26A@cam.ac.uk> <5541FE85.3050707@in.tum.de>

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.

**Follow-Ups**:**Re: [isabelle] ln on negative numbers***From:*Manuel Eberl

**References**:**[isabelle] ln on negative numbers***From:*Manuel Eberl

**Re: [isabelle] ln on negative numbers***From:*Larry Paulson

**Re: [isabelle] ln on negative numbers***From:*Manuel Eberl

- Previous by Date: Re: [isabelle] libisabelle: Small Scala library to communicate with Isabelle
- Next by Date: Re: [isabelle] ln on negative numbers
- Previous by Thread: Re: [isabelle] ln on negative numbers
- Next by Thread: Re: [isabelle] ln on negative numbers
- Cl-isabelle-users April 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list