[isabelle-dev] complex argument function(s)

Dr A. Koutsoukou-Argyraki ak2110 at cam.ac.uk
Thu Jul 1 16:05:47 CEST 2021

yes, arg z is multi-valued,
and N measures how many rotations around the axis you do, while Arg z is 
just the principal value.

And I should have written N \in \int (not N \in \nat) in my previous 


On 2021-07-01 09:37, Manuel Eberl wrote:
> On 01/07/2021 03:09, Dr A. Koutsoukou-Argyraki wrote:
>> Usually in the literature it's  -\pi < Arg z \leq \pi
>> while arg z = Arg z + 2 \pi N, where N \in \nat
> I don't understand what the second one means. Is this a multi-valued
> function or what does the "N" mean here?

More information about the isabelle-dev mailing list