mathlib documentation

analysis.special_functions.complex.arg

The argument of a complex number. #

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

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.arg_le_pi (x : ) :
theorem complex.neg_pi_lt_arg (x : ) :
theorem complex.arg_eq_arg_neg_add_pi_of_im_nonneg_of_re_neg {x : } (hxr : x.re < 0) (hxi : 0 x.im) :
x.arg = (-x).arg + π
theorem complex.arg_eq_arg_neg_sub_pi_of_im_neg_of_re_neg {x : } (hxr : x.re < 0) (hxi : x.im < 0) :
x.arg = (-x).arg - π
@[simp]
theorem complex.arg_zero  :
0.arg = 0
@[simp]
theorem complex.arg_one  :
1.arg = 0
@[simp]
theorem complex.arg_neg_one  :
(-1).arg = π
@[simp]
theorem complex.arg_I  :
@[simp]
theorem complex.arg_neg_I  :
theorem complex.cos_arg {x : } (hx : x 0) :
theorem complex.tan_arg {x : } :
theorem complex.arg_cos_add_sin_mul_I {x : } (hx₁ : -π < x) (hx₂ : x π) :
theorem complex.arg_eq_arg_iff {x y : } (hx : x 0) (hy : y 0) :
theorem complex.arg_real_mul (x : ) {r : } (hr : 0 < r) :
((r) * x).arg = x.arg
theorem complex.ext_abs_arg {x y : } (h₁ : complex.abs x = complex.abs y) (h₂ : x.arg = y.arg) :
x = y
theorem complex.arg_of_real_of_nonneg {x : } (hx : 0 x) :
x.arg = 0
theorem complex.arg_eq_pi_iff {z : } :
z.arg = π z.re < 0 z.im = 0
theorem complex.arg_of_real_of_neg {x : } (hx : x < 0) :