Yesterday I renamed arg -> Arg along with most of the arg_ theorems (though we still have arg_unique and Arg_unique).
I noticed some useful-looking basic lemmas about Arg in Stirling_Formula/Gamma_Asymptotics.thy (added to the AFP by Manuel in 2016) that we might bring into the libraries. Any comments? Larry > On 25 Jun 2021, at 21:28, Lawrence Paulson <[email protected]> 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
