mathlib

923923f1 - feat(analysis/special_functions/complex/arg): `arg_mul`, `arg_div` lemmas (#11903)

feat(analysis/special_functions/complex/arg): `arg_mul`, `arg_div` lemmas (#11903) Add lemmas about `(arg (x * y) : real.angle)` and `(arg (x / y) : real.angle)`, along with preparatory lemmas that are like those such as `arg_mul_cos_add_sin_mul_I` but either don't require the real argument to be in `Ioc (-π) π` or that take a `real.angle` argument. I didn't add any lemmas about `arg (x * y)` or `arg (x / y)` as a real; if such lemmas prove useful in future, it might make sense to deduce them from the `real.angle` versions.