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 #

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 : ℂ} :

same_ray ℝ x y ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg

theorem complex.same_ray_iff_arg_div_eq_zero {x y : ℂ} :

same_ray ℝ x y ↔ (x / y).arg = 0

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_sub_eq_iff {x y : ℂ} :

complex.abs (x - y) = |complex.abs x - complex.abs y| ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg

theorem complex.same_ray_of_arg_eq {x y : ℂ} (h : x.arg = y.arg) :

same_ray ℝ x y

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∥