Commit 2022-02-10 20:43 923923f1

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.