[isabelle-dev] complex argument function(s)

[Dr A. Koutsoukou-Argyraki]

I was only commenting on the most common naming convention within the 
maths literature regarding arg VS Arg.

Best,
Angeliki


On 2021-07-01 15:07, Manuel Eberl wrote:
> Well, that does not make much sense in Isabelle/HOL. HOL doesn't have
> multivalued functions.
> 
> We can only emulate such things with e.g. relations, which is what
> is_Arg does.
> 
> Manuel
> 
> 
> On 01/07/2021 16:05, Dr A. Koutsoukou-Argyraki wrote:
>> 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
>> message!
>> 
>> Best,
>> Angeliki
>> 
>> 
>> 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?
>>>