mathlib3 documentation

analysis.complex.arg

Rays in the complex numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 the same argument, then the triangle inequality is an equality.

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‖