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 could vary)
A suggestion would be to follow the above literature convention in the Library definitions too
(if practical enough) Best, Angeliki On 2021-06-25 21:28, Lawrence Paulson wrote:
I’ve just noticed that we define both arg and Arg, the latter in Complex_Transcendental. 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). Larry _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
