feat(analysis/complex/arg): same_ray_iff_arg_div_eq_zero (#16218)

Add the lemma that `same_ray ℝ x y ↔ arg (x / y) = 0`.

src/analysis/complex/arg.lean

@@ -37,6 +37,14 @@ begin
   rw [mul_comm, eq_comm]
 end
 
+lemma same_ray_iff_arg_div_eq_zero : same_ray ℝ x y ↔ arg (x / y) = 0 :=
+begin
+  rw [←real.angle.to_real_zero, ←arg_coe_angle_eq_iff_eq_to_real, same_ray_iff],
+  by_cases hx : x = 0, { simp [hx] },
+  by_cases hy : y = 0, { simp [hy] },
+  simp [hx, hy, arg_div_coe_angle, sub_eq_zero]
+end
+
 lemma abs_add_eq_iff : (x + y).abs = x.abs + y.abs ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg :=
 same_ray_iff_norm_add.symm.trans same_ray_iff