# mathlibdocumentation

analysis.complex.arg

# Rays in the complex numbers #

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

## Main statements #

• complex.same_ray_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 different argument, then the triangle inequality becomes strict.
theorem complex.same_ray_iff {x y : } :
y x = 0 y = 0 x.arg = y.arg
theorem complex.abs_add_eq_iff {x y : } :
complex.abs (x + y) = x = 0 y = 0 x.arg = y.arg
theorem complex.abs_sub_eq_iff {x y : } :
complex.abs (x - y) = x = 0 y = 0 x.arg = y.arg
theorem complex.same_ray_of_arg_eq {x y : } (h : x.arg = y.arg) :
y
theorem complex.abs_add_eq {x y : } (h : x.arg = y.arg) :
complex.abs (x + y) =
theorem complex.abs_sub_eq {x y : } (h : x.arg = y.arg) :
complex.abs (x - y) =