[isabelle-dev] complex argument function(s)

[Manuel Eberl]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5574 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20210701/dce17721/attachment.bin>