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 ∨ Complex.arg x = Complex.arg y

theorem Complex.sameRay_iff_arg_div_eq_zero {x : ℂ} {y : ℂ} : SameRay ℝ x y ↔ Complex.arg (x / y) = 0

theorem Complex.abs_add_eq_iff {x : ℂ} {y : ℂ} : Complex.abs (x + y) = Complex.abs x + Complex.abs y ↔ x = 0 ∨ y = 0 ∨ Complex.arg x = Complex.arg y

theorem Complex.abs_sub_eq_iff {x : ℂ} {y : ℂ} : Complex.abs (x - y) = |Complex.abs x - Complex.abs y| ↔ x = 0 ∨ y = 0 ∨ Complex.arg x = Complex.arg y

theorem Complex.sameRay_of_arg_eq {x : ℂ} {y : ℂ} (h : Complex.arg x = Complex.arg y) : SameRay ℝ x y

theorem Complex.abs_add_eq {x : ℂ} {y : ℂ} (h : Complex.arg x = Complex.arg y) : Complex.abs (x + y) = Complex.abs x + Complex.abs y

theorem Complex.abs_sub_eq {x : ℂ} {y : ℂ} (h : Complex.arg x = Complex.arg y) : Complex.abs (x - y) = ‖Complex.abs x - Complex.abs y‖