[isabelle-dev] complex argument function(s)
Dr A. Koutsoukou-Argyraki
ak2110 at cam.ac.uk
Thu Jul 1 03:09:48 CEST 2021
Usually in the literature it's -\pi < Arg z \leq \pi
while arg z = Arg z + 2 \pi N, where N \in \nat
(though sometimes several authors may use these interchangeably or it
A suggestion would be to follow the above literature convention in the
Library definitions too
(if practical enough)
On 2021-06-25 21:28, Lawrence Paulson wrote:
> I’ve just noticed that we define both arg and Arg, the latter in
> The definitions are different but arg z = Arg z holds unconditionally.
> It looks like a historical accident, maybe arg was introduced in the
> 1990s and forgotten about.
> Interestingly enough, arg is used far more despite there being almost
> nothing proved about it. Some lemmas are proved in
> Complex_Geometry/More_Complex.thy, and many occurrences of “arg” are
> simply variables.
> This is a mess. Any suggestions? Maybe Arg could (temporarily) be made
> an abbreviation for arg. Arg is the usual of the function (principal
> value of the argument).
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev