# Rays in the complex numbers #

This file links the definition SameRay ℝ x y with the equality of arguments of complex numbers, the usual way this is considered.

## Main statements #

• Complex.sameRay_iff : Two complex numbers are on the same ray iff one of them is zero, or they have the same argument.
• Complex.abs_add_eq/Complex.abs_sub_eq: If two non zero complex numbers have the same argument, then the triangle inequality is an equality.
theorem Complex.sameRay_iff {x : } {y : } :
SameRay x y x = 0 y = 0 x.arg = y.arg
theorem Complex.sameRay_iff_arg_div_eq_zero {x : } {y : } :
SameRay x y (x / y).arg = 0
theorem Complex.abs_add_eq_iff {x : } {y : } :
Complex.abs (x + y) = Complex.abs x + Complex.abs y x = 0 y = 0 x.arg = y.arg
theorem Complex.abs_sub_eq_iff {x : } {y : } :
Complex.abs (x - y) = |Complex.abs x - Complex.abs y| x = 0 y = 0 x.arg = y.arg
theorem Complex.sameRay_of_arg_eq {x : } {y : } (h : x.arg = y.arg) :
theorem Complex.abs_add_eq {x : } {y : } (h : x.arg = y.arg) :
Complex.abs (x + y) = Complex.abs x + Complex.abs y
theorem Complex.abs_sub_eq {x : } {y : } (h : x.arg = y.arg) :
Complex.abs (x - y) = Complex.abs x - Complex.abs y