Commit 2022-01-17 10:14 079fb166

feat(analysis/special_functions/complex/arg): arg_neg lemmas (#11503) Add lemmas about the value of arg (-x): one each for positive and negative sign of x.im, two iff lemmas saying exactly when it's equal to arg x - π or arg x + π, and a simpler lemma giving the value of (arg (-x) : real.angle) for any nonzero x. These replace the previous lemmas arg_eq_arg_neg_add_pi_of_im_nonneg_of_re_neg and arg_eq_arg_neg_sub_pi_of_im_neg_of_re_neg, which are strictly less general (they have a hypothesis x.re < 0 that's not needed unless the imaginary part is 0). Those two lemmas are unused in current mathlib (they were used in the proof of cos_arg before the golfing in #10365) and it seems reasonable to me to replace them with the more general lemmas.