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.