Commit 2021-11-20 11:30 618447fa

feat(analysis/special_functions/complex/arg): review, golf, lemmas (#10365)

• add |z| * exp (arg z * I) = z;
• reorder theorems to help golfing;
• prove formulas for arg z in terms of arccos (re z / abs z) in cases 0 < im z and im z < 0;
• use them to golf continuity of arg.