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.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_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∥