mathlib

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

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`.