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.norm_add_eq_iff {x y : ℂ} : ‖x + y‖ = ‖x‖ + ‖y‖ ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg

theorem Complex.norm_sub_eq_iff {x y : ℂ} : ‖x - y‖ = |‖x‖ - ‖y‖| ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg

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

theorem Complex.norm_add_eq {x y : ℂ} (h : x.arg = y.arg) : ‖x + y‖ = ‖x‖ + ‖y‖

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

@[deprecated Complex.norm_add_eq_iff (since := "2025-02-17")]

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

Alias of Complex.norm_add_eq_iff.

@[deprecated Complex.norm_sub_eq_iff (since := "2025-02-17")]

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

Alias of Complex.norm_sub_eq_iff.

@[deprecated Complex.norm_add_eq (since := "2025-02-17")]

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

Alias of Complex.norm_add_eq.

@[deprecated Complex.norm_sub_eq (since := "2025-02-17")]

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

Alias of Complex.norm_sub_eq.