arg): `same_ray_iff_arg_div_eq_zero` (#16218)

Commit

3 years ago

feat(analysis/complex/arg): `same_ray_iff_arg_div_eq_zero` (#16218) Add the lemma that `same_ray ℝ x y ↔ arg (x / y) = 0`.

Author

jsm28

Parents