# The argument of a complex number. #

We define arg : ℂ → ℝ, returning 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
• x.arg = if 0 x.re then (x.im / Complex.abs x).arcsin else if 0 x.im then ((-x).im / Complex.abs x).arcsin + Real.pi else ((-x).im / Complex.abs x).arcsin - Real.pi
Instances For
theorem Complex.sin_arg (x : ) :
x.arg.sin = x.im / Complex.abs x
theorem Complex.cos_arg {x : } (hx : x 0) :
x.arg.cos = x.re / Complex.abs x
@[simp]
theorem Complex.abs_mul_exp_arg_mul_I (x : ) :
(Complex.abs x) * (x.arg * Complex.I).exp = x
@[simp]
theorem Complex.abs_mul_cos_add_sin_mul_I (x : ) :
(Complex.abs x) * ((x.arg).cos + (x.arg).sin * Complex.I) = x
@[simp]
theorem Complex.abs_mul_cos_arg (x : ) :
Complex.abs x * x.arg.cos = x.re
@[simp]
theorem Complex.abs_mul_sin_arg (x : ) :
Complex.abs x * x.arg.sin = x.im
theorem Complex.abs_eq_one_iff (z : ) :
Complex.abs z = 1 ∃ (θ : ), ().exp = z
@[simp]
theorem Complex.range_exp_mul_I :
(Set.range fun (x : ) => ().exp) =
theorem Complex.arg_mul_cos_add_sin_mul_I {r : } (hr : 0 < r) {θ : } (hθ : ) :
(r * ((θ).cos + (θ).sin * Complex.I)).arg = θ
theorem Complex.arg_cos_add_sin_mul_I {θ : } (hθ : ) :
((θ).cos + (θ).sin * Complex.I).arg = θ
theorem Complex.arg_exp_mul_I (θ : ) :
().exp.arg = toIocMod () θ
@[simp]
theorem Complex.arg_zero :
= 0
theorem Complex.ext_abs_arg {x : } {y : } (h₁ : Complex.abs x = Complex.abs y) (h₂ : x.arg = y.arg) :
x = y
theorem Complex.ext_abs_arg_iff {x : } {y : } :
x = y Complex.abs x = Complex.abs y x.arg = y.arg
theorem Complex.arg_mem_Ioc (z : ) :
z.arg
@[simp]
theorem Complex.arg_le_pi (x : ) :
x.arg Real.pi
theorem Complex.neg_pi_lt_arg (x : ) :
< x.arg
@[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_mul_real {r : } (hr : 0 < r) (x : ) :
(x * r).arg = x.arg
theorem Complex.arg_eq_arg_iff {x : } {y : } (hx : x 0) (hy : y 0) :
x.arg = y.arg (Complex.abs y) / (Complex.abs x) * x = y
@[simp]
theorem Complex.arg_one :
= 0
@[simp]
theorem Complex.arg_neg_one :
(-1).arg = Real.pi
@[simp]
theorem Complex.arg_I :
@[simp]
theorem Complex.arg_neg_I :
.arg = -()
@[simp]
theorem Complex.tan_arg (x : ) :
x.arg.tan = x.im / x.re
theorem Complex.arg_ofReal_of_nonneg {x : } (hx : 0 x) :
(x).arg = 0
@[simp]
theorem Complex.natCast_arg {n : } :
(n).arg = 0
@[simp]
theorem Complex.ofNat_arg {n : } [n.AtLeastTwo] :
().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_ofReal_of_neg {x : } (hx : x < 0) :
(x).arg = Real.pi
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 = -() z.re = 0 z.im < 0
theorem Complex.arg_of_re_nonneg {x : } (hx : 0 x.re) :
x.arg = (x.im / Complex.abs x).arcsin
theorem Complex.arg_of_re_neg_of_im_nonneg {x : } (hx_re : x.re < 0) (hx_im : 0 x.im) :
x.arg = ((-x).im / Complex.abs x).arcsin + Real.pi
theorem Complex.arg_of_re_neg_of_im_neg {x : } (hx_re : x.re < 0) (hx_im : x.im < 0) :
x.arg = ((-x).im / Complex.abs x).arcsin - Real.pi
theorem Complex.arg_of_im_nonneg_of_ne_zero {z : } (h₁ : 0 z.im) (h₂ : z 0) :
z.arg = (z.re / Complex.abs z).arccos
theorem Complex.arg_of_im_pos {z : } (hz : 0 < z.im) :
z.arg = (z.re / Complex.abs z).arccos
theorem Complex.arg_of_im_neg {z : } (hz : z.im < 0) :
z.arg = -(z.re / Complex.abs z).arccos
theorem Complex.arg_conj (x : ) :
(() x).arg = if x.arg = Real.pi then Real.pi else -x.arg
theorem Complex.arg_inv (x : ) :
x⁻¹.arg = if x.arg = Real.pi then Real.pi else -x.arg
@[simp]
theorem Complex.abs_arg_inv (x : ) :
|x⁻¹.arg| = |x.arg|
theorem Complex.abs_eq_one_iff' {x : } :
Complex.abs x = 1 θ, ().exp = x
theorem Complex.image_exp_Ioc_eq_sphere :
(fun (θ : ) => ().exp) '' =
theorem Complex.arg_le_pi_div_two_iff {z : } :
z.arg 0 z.re z.im < 0
theorem Complex.neg_pi_div_two_le_arg_iff {z : } :
-() z.arg 0 z.re 0 z.im
theorem Complex.neg_pi_div_two_lt_arg_iff {z : } :
-() < z.arg 0 < z.re 0 z.im
theorem Complex.arg_lt_pi_div_two_iff {z : } :
z.arg < 0 < z.re z.im < 0 z = 0
@[simp]
theorem Complex.abs_arg_le_pi_div_two_iff {z : } :
|z.arg| 0 z.re
@[simp]
theorem Complex.abs_arg_lt_pi_div_two_iff {z : } :
|z.arg| < 0 < z.re z = 0
@[simp]
theorem Complex.arg_conj_coe_angle (x : ) :
(() x).arg = -x.arg
@[simp]
theorem Complex.arg_inv_coe_angle (x : ) :
x⁻¹.arg = -x.arg
theorem Complex.arg_neg_eq_arg_sub_pi_of_im_pos {x : } (hi : 0 < x.im) :
(-x).arg = x.arg - Real.pi
theorem Complex.arg_neg_eq_arg_add_pi_of_im_neg {x : } (hi : x.im < 0) :
(-x).arg = x.arg + Real.pi
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) :
(-x).arg = x.arg +
theorem Complex.arg_mul_cos_add_sin_mul_I_eq_toIocMod {r : } (hr : 0 < r) (θ : ) :
(r * ((θ).cos + (θ).sin * Complex.I)).arg =
theorem Complex.arg_cos_add_sin_mul_I_eq_toIocMod (θ : ) :
((θ).cos + (θ).sin * Complex.I).arg =
theorem Complex.arg_mul_cos_add_sin_mul_I_sub {r : } (hr : 0 < r) (θ : ) :
(r * ((θ).cos + (θ).sin * Complex.I)).arg - θ = * () / ()
theorem Complex.arg_cos_add_sin_mul_I_sub (θ : ) :
((θ).cos + (θ).sin * Complex.I).arg - θ = * () / ()
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_cos_add_sin_mul_I_coe_angle (θ : Real.Angle) :
(θ.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_toReal_eq_arg (z : ) :
(z.arg).toReal = z.arg
theorem Complex.arg_coe_angle_eq_iff_eq_toReal {z : } {θ : Real.Angle} :
z.arg = θ z.arg = θ.toReal
@[simp]
theorem Complex.arg_coe_angle_eq_iff {x : } {y : } :
x.arg = y.arg x.arg = y.arg
theorem Complex.arg_mul_eq_add_arg_iff {x : } {y : } (hx₀ : x 0) (hy₀ : y 0) :
(x * y).arg = x.arg + y.arg x.arg + y.arg
theorem Complex.arg_mul {x : } {y : } (hx₀ : x 0) (hy₀ : y 0) :
x.arg + y.arg (x * y).arg = x.arg + y.arg

Alias of the reverse direction of Complex.arg_mul_eq_add_arg_iff.

An alternative description of the slit plane as consisting of nonzero complex numbers whose argument is not π.

theorem Complex.slitPlane_arg_ne_pi {z : } (hz : ) :
z.arg Real.pi
theorem Complex.arg_eq_nhds_of_re_pos {x : } (hx : 0 < x.re) :
Complex.arg =ᶠ[nhds x] fun (x : ) => (x.im / Complex.abs x).arcsin
theorem Complex.arg_eq_nhds_of_re_neg_of_im_pos {x : } (hx_re : x.re < 0) (hx_im : 0 < x.im) :
Complex.arg =ᶠ[nhds x] fun (x : ) => ((-x).im / Complex.abs x).arcsin + Real.pi
theorem Complex.arg_eq_nhds_of_re_neg_of_im_neg {x : } (hx_re : x.re < 0) (hx_im : x.im < 0) :
Complex.arg =ᶠ[nhds x] fun (x : ) => ((-x).im / Complex.abs x).arcsin - Real.pi
theorem Complex.arg_eq_nhds_of_im_pos {z : } (hz : 0 < z.im) :
Complex.arg =ᶠ[nhds z] fun (x : ) => (x.re / Complex.abs x).arccos
theorem Complex.arg_eq_nhds_of_im_neg {z : } (hz : z.im < 0) :
Complex.arg =ᶠ[nhds z] fun (x : ) => -(x.re / Complex.abs x).arccos
theorem Complex.continuousAt_arg {x : } (h : ) :
theorem Complex.tendsto_arg_nhdsWithin_im_neg_of_re_neg_of_im_zero {z : } (hre : z.re < 0) (him : z.im = 0) :
Filter.Tendsto Complex.arg (nhdsWithin z {z : | z.im < 0}) ()
theorem Complex.continuousWithinAt_arg_of_re_neg_of_im_zero {z : } (hre : z.re < 0) (him : z.im = 0) :