# mathlib3documentation

analysis.special_functions.complex.arg

# The argument of a complex number. #

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

We define arg : ℂ → ℝ, returing a real number in the range (-π, π], such that for x ≠ 0, sin (arg x) = x.im / x.abs and cos (arg x) = x.re / x.abs, while arg 0 defaults to 0

noncomputable def complex.arg (x : ) :

arg returns values in the range (-π, π], such that for x ≠ 0, sin (arg x) = x.im / x.abs and cos (arg x) = x.re / x.abs, arg 0 defaults to 0

Equations
theorem complex.sin_arg (x : ) :
= x.im /
theorem complex.cos_arg {x : } (hx : x 0) :
= x.re /
theorem complex.abs_eq_one_iff (z : ) :
(θ : ), cexp (θ * complex.I) = z
@[simp]
theorem complex.range_exp_mul_I  :
set.range (λ (x : ), cexp (x * complex.I)) =
theorem complex.arg_mul_cos_add_sin_mul_I {r : } (hr : 0 < r) {θ : } (hθ : θ ) :
(r * + .arg = θ
theorem complex.arg_cos_add_sin_mul_I {θ : } (hθ : θ ) :
.arg = θ
@[simp]
theorem complex.arg_zero  :
0.arg = 0
theorem complex.ext_abs_arg {x y : } (h₁ : = ) (h₂ : x.arg = y.arg) :
x = y
theorem complex.ext_abs_arg_iff {x y : } :
x = y x.arg = y.arg
theorem complex.arg_mem_Ioc (z : ) :
@[simp]
theorem complex.range_arg  :
theorem complex.arg_le_pi (x : ) :
theorem complex.neg_pi_lt_arg (x : ) :
theorem complex.abs_arg_le_pi (z : ) :
@[simp]
theorem complex.arg_nonneg_iff {z : } :
0 z.arg 0 z.im
@[simp]
theorem complex.arg_neg_iff {z : } :
z.arg < 0 z.im < 0
theorem complex.arg_real_mul (x : ) {r : } (hr : 0 < r) :
(r * x).arg = x.arg
theorem complex.arg_eq_arg_iff {x y : } (hx : x 0) (hy : y 0) :
@[simp]
theorem complex.arg_one  :
1.arg = 0
@[simp]
theorem complex.arg_neg_one  :
@[simp]
theorem complex.arg_I  :
@[simp]
@[simp]
theorem complex.tan_arg (x : ) :
= x.im / x.re
theorem complex.arg_of_real_of_nonneg {x : } (hx : 0 x) :
x.arg = 0
theorem complex.arg_eq_zero_iff {z : } :
z.arg = 0 0 z.re z.im = 0
theorem complex.arg_eq_pi_iff {z : } :
z.re < 0 z.im = 0
theorem complex.arg_lt_pi_iff {z : } :
0 z.re z.im 0
theorem complex.arg_of_real_of_neg {x : } (hx : x < 0) :
theorem complex.arg_eq_pi_div_two_iff {z : } :
z.arg = z.re = 0 0 < z.im
theorem complex.arg_eq_neg_pi_div_two_iff {z : } :
z.arg = -(real.pi / 2) z.re = 0 z.im < 0
theorem complex.arg_of_re_nonneg {x : } (hx : 0 x.re) :
theorem complex.arg_of_re_neg_of_im_nonneg {x : } (hx_re : x.re < 0) (hx_im : 0 x.im) :
theorem complex.arg_of_re_neg_of_im_neg {x : } (hx_re : x.re < 0) (hx_im : x.im < 0) :
theorem complex.arg_of_im_nonneg_of_ne_zero {z : } (h₁ : 0 z.im) (h₂ : z 0) :
theorem complex.arg_of_im_pos {z : } (hz : 0 < z.im) :
theorem complex.arg_of_im_neg {z : } (hz : z.im < 0) :
theorem complex.arg_conj (x : ) :
theorem complex.arg_inv (x : ) :
theorem complex.arg_le_pi_div_two_iff {z : } :
z.arg 0 z.re z.im < 0
@[simp]
@[simp]
theorem complex.arg_conj_coe_angle (x : ) :
(( x).arg) = -(x.arg)
@[simp]
theorem complex.arg_neg_eq_arg_sub_pi_of_im_pos {x : } (hi : 0 < x.im) :
(-x).arg =
theorem complex.arg_neg_eq_arg_add_pi_of_im_neg {x : } (hi : x.im < 0) :
(-x).arg =
theorem complex.arg_neg_eq_arg_sub_pi_iff {x : } :
(-x).arg = 0 < x.im x.im = 0 x.re < 0
theorem complex.arg_neg_eq_arg_add_pi_iff {x : } :
(-x).arg = x.im < 0 x.im = 0 0 < x.re
theorem complex.arg_neg_coe_angle {x : } (hx : x 0) :
theorem complex.arg_mul_cos_add_sin_mul_I_eq_to_Ioc_mod {r : } (hr : 0 < r) (θ : ) :
(r * + .arg =
theorem complex.arg_mul_cos_add_sin_mul_I_sub {r : } (hr : 0 < r) (θ : ) :
(r * + .arg - θ = * (real.pi - θ) / (2 * real.pi)
theorem complex.arg_mul_cos_add_sin_mul_I_coe_angle {r : } (hr : 0 < r) (θ : real.angle) :
((r * ((θ.cos) + (θ.sin) * complex.I)).arg) = θ
theorem complex.arg_mul_coe_angle {x y : } (hx : x 0) (hy : y 0) :
((x * y).arg) = (x.arg) + (y.arg)
theorem complex.arg_div_coe_angle {x y : } (hx : x 0) (hy : y 0) :
((x / y).arg) = (x.arg) - (y.arg)
@[simp]
theorem complex.arg_coe_angle_eq_iff {x y : } :
(x.arg) = (y.arg) x.arg = y.arg
theorem complex.arg_eq_nhds_of_re_pos {x : } (hx : 0 < x.re) :
theorem complex.arg_eq_nhds_of_re_neg_of_im_pos {x : } (hx_re : x.re < 0) (hx_im : 0 < x.im) :
theorem complex.arg_eq_nhds_of_re_neg_of_im_neg {x : } (hx_re : x.re < 0) (hx_im : x.im < 0) :
theorem complex.arg_eq_nhds_of_im_pos {z : } (hz : 0 < z.im) :
theorem complex.arg_eq_nhds_of_im_neg {z : } (hz : z.im < 0) :
theorem complex.continuous_at_arg {x : } (h : 0 < x.re x.im 0) :
theorem complex.tendsto_arg_nhds_within_im_neg_of_re_neg_of_im_zero {z : } (hre : z.re < 0) (him : z.im = 0) :
{z : | z.im < 0}) (nhds (-real.pi))
theorem complex.continuous_within_at_arg_of_re_neg_of_im_zero {z : } (hre : z.re < 0) (him : z.im = 0) :
{z : | 0 z.im} z
theorem complex.tendsto_arg_nhds_within_im_nonneg_of_re_neg_of_im_zero {z : } (hre : z.re < 0) (him : z.im = 0) :
{z : | 0 z.im})
theorem complex.continuous_at_arg_coe_angle {x : } (h : x 0) :