mathlib documentation

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 #

theorem complex.same_ray_iff {x y : } :
same_ray x y x = 0 y = 0 x.arg = y.arg
theorem complex.abs_add_eq_iff {x y : } :
theorem complex.abs_sub_eq_iff {x y : } :
theorem complex.same_ray_of_arg_eq {x y : } (h : x.arg = y.arg) :
theorem complex.abs_add_eq {x y : } (h : x.arg = y.arg) :
theorem complex.abs_sub_eq {x y : } (h : x.arg = y.arg) :