mathlib

8ff5e113 - feat(analysis/special_functions/complex/arg): add complex.abs_eq_one_iff (#15125)

feat(analysis/special_functions/complex/arg): add complex.abs_eq_one_iff (#15125) This is a simpler formulation of `complex.range_exp_mul_I` below. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>