mathlib3 documentation

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.cos_arg {x : } (hx : x 0) :
@[simp]
theorem complex.arg_mul_cos_add_sin_mul_I {r : } (hr : 0 < r) {θ : } (hθ : θ set.Ioc (-real.pi) real.pi) :
@[simp]
theorem complex.arg_zero  :
0.arg = 0
theorem complex.ext_abs_arg {x y : } (h₁ : complex.abs x = complex.abs y) (h₂ : x.arg = y.arg) :
x = y
theorem complex.arg_le_pi (x : ) :
@[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]
@[simp]
@[simp]
theorem complex.tan_arg (x : ) :
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.arg = real.pi z.re < 0 z.im = 0
theorem complex.arg_lt_pi_iff {z : } :
z.arg < real.pi 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 = real.pi / 2 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_inv (x : ) :
@[simp]
@[simp]
@[simp]
theorem complex.arg_neg_eq_arg_sub_pi_of_im_pos {x : } (hi : 0 < x.im) :
theorem complex.arg_neg_eq_arg_add_pi_of_im_neg {x : } (hi : x.im < 0) :
theorem complex.arg_neg_eq_arg_sub_pi_iff {x : } :
(-x).arg = x.arg - real.pi 0 < x.im x.im = 0 x.re < 0
theorem complex.arg_neg_eq_arg_add_pi_iff {x : } :
(-x).arg = x.arg + real.pi 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_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_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) :