[isabelle-dev] complex argument function(s)

[Manuel Eberl]

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?

I agree with Larry that one of the two "arg" functions has to go. As for
which one, I have no preference. Making one of them into an abbreviation
sounds reasonable, although I am not sure if it really is less work than
just replacing it in one go immediately.

Note that we also have "is_Arg" and "Arg2pi", so perhaps "Arg" would be
more consistent than "arg".

Manuel

-------------- 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/fbb074a7/attachment.bin>