*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] ln on negative numbers*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Thu, 30 Apr 2015 17:09:12 +0200*In-reply-to*: <06E3E158-C505-462D-94B3-E229B3F32BC4@cam.ac.uk>*References*: <5540E488.6070106@in.tum.de> <7280EAEA-8715-472E-8B9E-6C11AC41F26A@cam.ac.uk> <5541FE85.3050707@in.tum.de> <06E3E158-C505-462D-94B3-E229B3F32BC4@cam.ac.uk>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.6.0

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. >

**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

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

- Previous by Date: Re: [isabelle] ln on negative numbers
- Next by Date: Re: [isabelle] apply simp: Tactic failed
- Previous by Thread: Re: [isabelle] ln on negative numbers
- Next by Thread: Re: [isabelle] apply simp: Tactic failed
- 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