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

• One or more equations did not get rendered due to their size.

theorem Complex.sin_arg (x : ℂ) : Real.sin (Complex.arg x) = x.im / Complex.abs x

theorem Complex.cos_arg {x : ℂ} (hx : x ≠ 0) : Real.cos (Complex.arg x) = x.re / Complex.abs x

@[simp]

theorem Complex.abs_mul_exp_arg_mul_I (x : ℂ) : ↑(Complex.abs x) * Complex.exp (↑(Complex.arg x) * Complex.I) = x

@[simp]

theorem Complex.abs_mul_cos_add_sin_mul_I (x : ℂ) : ↑(Complex.abs x) * (Complex.cos ↑(Complex.arg x) + Complex.sin ↑(Complex.arg x) * Complex.I) = x

@[simp]

theorem Complex.abs_mul_cos_arg (x : ℂ) : Complex.abs x * Real.cos (Complex.arg x) = x.re

@[simp]

theorem Complex.abs_mul_sin_arg (x : ℂ) : Complex.abs x * Real.sin (Complex.arg x) = x.im

theorem Complex.abs_eq_one_iff (z : ℂ) : Complex.abs z = 1 ↔ ∃ (θ : ℝ), Complex.exp (↑θ * Complex.I) = z

@[simp]

theorem Complex.range_exp_mul_I : (Set.range fun (x : ℝ) => Complex.exp (↑x * Complex.I)) = Metric.sphere 0 1

theorem Complex.arg_mul_cos_add_sin_mul_I {r : ℝ} (hr : 0 < r) {θ : ℝ} (hθ : θ ∈ Set.Ioc (-Real.pi) Real.pi) : Complex.arg (↑r * (Complex.cos ↑θ + Complex.sin ↑θ * Complex.I)) = θ

theorem Complex.arg_cos_add_sin_mul_I {θ : ℝ} (hθ : θ ∈ Set.Ioc (-Real.pi) Real.pi) : Complex.arg (Complex.cos ↑θ + Complex.sin ↑θ * Complex.I) = θ

theorem Complex.arg_exp_mul_I (θ : ℝ) : Complex.arg (Complex.exp (↑θ * Complex.I)) = toIocMod ⋯ (-Real.pi) θ

@[simp]

theorem Complex.arg_zero : Complex.arg 0 = 0

theorem Complex.ext_abs_arg {x : ℂ} {y : ℂ} (h₁ : Complex.abs x = Complex.abs y) (h₂ : Complex.arg x = Complex.arg y) : x = y

theorem Complex.ext_abs_arg_iff {x : ℂ} {y : ℂ} : x = y ↔ Complex.abs x = Complex.abs y ∧ Complex.arg x = Complex.arg y

theorem Complex.arg_mem_Ioc (z : ℂ) : Complex.arg z ∈ Set.Ioc (-Real.pi) Real.pi

@[simp]

theorem Complex.range_arg : Set.range Complex.arg = Set.Ioc (-Real.pi) Real.pi

theorem Complex.arg_le_pi (x : ℂ) : Complex.arg x ≤ Real.pi

theorem Complex.neg_pi_lt_arg (x : ℂ) : -Real.pi < Complex.arg x

theorem Complex.abs_arg_le_pi (z : ℂ) : |Complex.arg z| ≤ Real.pi

@[simp]

theorem Complex.arg_nonneg_iff {z : ℂ} : 0 ≤ Complex.arg z ↔ 0 ≤ z.im

@[simp]

theorem Complex.arg_neg_iff {z : ℂ} : Complex.arg z < 0 ↔ z.im < 0

theorem Complex.arg_real_mul (x : ℂ) {r : ℝ} (hr : 0 < r) : Complex.arg (↑r * x) = Complex.arg x

theorem Complex.arg_mul_real {r : ℝ} (hr : 0 < r) (x : ℂ) : Complex.arg (x * ↑r) = Complex.arg x

theorem Complex.arg_eq_arg_iff {x : ℂ} {y : ℂ} (hx : x ≠ 0) (hy : y ≠ 0) : Complex.arg x = Complex.arg y ↔ ↑(Complex.abs y) / ↑(Complex.abs x) * x = y

@[simp]

theorem Complex.arg_one : Complex.arg 1 = 0

@[simp]

theorem Complex.arg_neg_one : Complex.arg (-1) = Real.pi

@[simp]

theorem Complex.arg_I : Complex.arg Complex.I = Real.pi / 2

@[simp]

theorem Complex.arg_neg_I : Complex.arg (-Complex.I) = -(Real.pi / 2)

@[simp]

theorem Complex.tan_arg (x : ℂ) : Real.tan (Complex.arg x) = x.im / x.re

theorem Complex.arg_ofReal_of_nonneg {x : ℝ} (hx : 0 ≤ x) : Complex.arg ↑x = 0

@[simp]

theorem Complex.natCast_arg {n : ℕ} : Complex.arg ↑n = 0

@[simp]

theorem Complex.ofNat_arg {n : ℕ} [Nat.AtLeastTwo n] : Complex.arg (OfNat.ofNat n) = 0

theorem Complex.arg_eq_zero_iff {z : ℂ} : Complex.arg z = 0 ↔ 0 ≤ z.re ∧ z.im = 0

theorem Complex.arg_eq_zero_iff_zero_le {z : ℂ} : Complex.arg z = 0 ↔ 0 ≤ z

theorem Complex.arg_eq_pi_iff {z : ℂ} : Complex.arg z = Real.pi ↔ z.re < 0 ∧ z.im = 0

theorem Complex.arg_eq_pi_iff_lt_zero {z : ℂ} : Complex.arg z = Real.pi ↔ z < 0

theorem Complex.arg_lt_pi_iff {z : ℂ} : Complex.arg z < Real.pi ↔ 0 ≤ z.re ∨ z.im ≠ 0

theorem Complex.arg_ofReal_of_neg {x : ℝ} (hx : x < 0) : Complex.arg ↑x = Real.pi

theorem Complex.arg_eq_pi_div_two_iff {z : ℂ} : Complex.arg z = Real.pi / 2 ↔ z.re = 0 ∧ 0 < z.im

theorem Complex.arg_eq_neg_pi_div_two_iff {z : ℂ} : Complex.arg z = -(Real.pi / 2) ↔ z.re = 0 ∧ z.im < 0

theorem Complex.arg_of_re_nonneg {x : ℂ} (hx : 0 ≤ x.re) : Complex.arg x = Real.arcsin (x.im / Complex.abs x)

theorem Complex.arg_of_re_neg_of_im_nonneg {x : ℂ} (hx_re : x.re < 0) (hx_im : 0 ≤ x.im) : Complex.arg x = Real.arcsin ((-x).im / Complex.abs x) + Real.pi

theorem Complex.arg_of_re_neg_of_im_neg {x : ℂ} (hx_re : x.re < 0) (hx_im : x.im < 0) : Complex.arg x = Real.arcsin ((-x).im / Complex.abs x) - Real.pi

theorem Complex.arg_of_im_nonneg_of_ne_zero {z : ℂ} (h₁ : 0 ≤ z.im) (h₂ : z ≠ 0) : Complex.arg z = Real.arccos (z.re / Complex.abs z)

theorem Complex.arg_of_im_pos {z : ℂ} (hz : 0 < z.im) : Complex.arg z = Real.arccos (z.re / Complex.abs z)

theorem Complex.arg_of_im_neg {z : ℂ} (hz : z.im < 0) : Complex.arg z = -Real.arccos (z.re / Complex.abs z)

theorem Complex.arg_conj (x : ℂ) : Complex.arg ((starRingEnd ℂ) x) = if Complex.arg x = Real.pi then Real.pi else -Complex.arg x

theorem Complex.arg_inv (x : ℂ) : Complex.arg x⁻¹ = if Complex.arg x = Real.pi then Real.pi else -Complex.arg x

@[simp]

theorem Complex.abs_arg_inv (x : ℂ) : |Complex.arg x⁻¹| = |Complex.arg x|

theorem Complex.abs_eq_one_iff' {x : ℂ} : Complex.abs x = 1 ↔ ∃ θ ∈ Set.Ioc (-Real.pi) Real.pi, Complex.exp (↑θ * Complex.I) = x

theorem Complex.image_exp_Ioc_eq_sphere : (fun (θ : ℝ) => Complex.exp (↑θ * Complex.I)) '' Set.Ioc (-Real.pi) Real.pi = Metric.sphere 0 1

theorem Complex.arg_le_pi_div_two_iff {z : ℂ} : Complex.arg z ≤ Real.pi / 2 ↔ 0 ≤ z.re ∨ z.im < 0

theorem Complex.neg_pi_div_two_le_arg_iff {z : ℂ} : -(Real.pi / 2) ≤ Complex.arg z ↔ 0 ≤ z.re ∨ 0 ≤ z.im

theorem Complex.neg_pi_div_two_lt_arg_iff {z : ℂ} : -(Real.pi / 2) < Complex.arg z ↔ 0 < z.re ∨ 0 ≤ z.im

theorem Complex.arg_lt_pi_div_two_iff {z : ℂ} : Complex.arg z < Real.pi / 2 ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0

@[simp]

theorem Complex.abs_arg_le_pi_div_two_iff {z : ℂ} : |Complex.arg z| ≤ Real.pi / 2 ↔ 0 ≤ z.re

@[simp]

theorem Complex.abs_arg_lt_pi_div_two_iff {z : ℂ} : |Complex.arg z| < Real.pi / 2 ↔ 0 < z.re ∨ z = 0

@[simp]

theorem Complex.arg_conj_coe_angle (x : ℂ) : ↑(Complex.arg ((starRingEnd ℂ) x)) = -↑(Complex.arg x)

@[simp]

theorem Complex.arg_inv_coe_angle (x : ℂ) : ↑(Complex.arg x⁻¹) = -↑(Complex.arg x)

theorem Complex.arg_neg_eq_arg_sub_pi_of_im_pos {x : ℂ} (hi : 0 < x.im) : Complex.arg (-x) = Complex.arg x - Real.pi

theorem Complex.arg_neg_eq_arg_add_pi_of_im_neg {x : ℂ} (hi : x.im < 0) : Complex.arg (-x) = Complex.arg x + Real.pi

theorem Complex.arg_neg_eq_arg_sub_pi_iff {x : ℂ} : Complex.arg (-x) = Complex.arg x - Real.pi ↔ 0 < x.im ∨ x.im = 0 ∧ x.re < 0

theorem Complex.arg_neg_eq_arg_add_pi_iff {x : ℂ} : Complex.arg (-x) = Complex.arg x + Real.pi ↔ x.im < 0 ∨ x.im = 0 ∧ 0 < x.re

theorem Complex.arg_neg_coe_angle {x : ℂ} (hx : x ≠ 0) : ↑(Complex.arg (-x)) = ↑(Complex.arg x) + ↑Real.pi

theorem Complex.arg_mul_cos_add_sin_mul_I_eq_toIocMod {r : ℝ} (hr : 0 < r) (θ : ℝ) : Complex.arg (↑r * (Complex.cos ↑θ + Complex.sin ↑θ * Complex.I)) = toIocMod Real.two_pi_pos (-Real.pi) θ

theorem Complex.arg_cos_add_sin_mul_I_eq_toIocMod (θ : ℝ) : Complex.arg (Complex.cos ↑θ + Complex.sin ↑θ * Complex.I) = toIocMod Real.two_pi_pos (-Real.pi) θ

theorem Complex.arg_mul_cos_add_sin_mul_I_sub {r : ℝ} (hr : 0 < r) (θ : ℝ) : Complex.arg (↑r * (Complex.cos ↑θ + Complex.sin ↑θ * Complex.I)) - θ = 2 * Real.pi * ↑⌊(Real.pi - θ) / (2 * Real.pi)⌋

theorem Complex.arg_cos_add_sin_mul_I_sub (θ : ℝ) : Complex.arg (Complex.cos ↑θ + Complex.sin ↑θ * Complex.I) - θ = 2 * Real.pi * ↑⌊(Real.pi - θ) / (2 * Real.pi)⌋

theorem Complex.arg_mul_cos_add_sin_mul_I_coe_angle {r : ℝ} (hr : 0 < r) (θ : Real.Angle) : ↑(Complex.arg (↑r * (↑(Real.Angle.cos θ) + ↑(Real.Angle.sin θ) * Complex.I))) = θ

theorem Complex.arg_cos_add_sin_mul_I_coe_angle (θ : Real.Angle) : ↑(Complex.arg (↑(Real.Angle.cos θ) + ↑(Real.Angle.sin θ) * Complex.I)) = θ

theorem Complex.arg_mul_coe_angle {x : ℂ} {y : ℂ} (hx : x ≠ 0) (hy : y ≠ 0) : ↑(Complex.arg (x * y)) = ↑(Complex.arg x) + ↑(Complex.arg y)

theorem Complex.arg_div_coe_angle {x : ℂ} {y : ℂ} (hx : x ≠ 0) (hy : y ≠ 0) : ↑(Complex.arg (x / y)) = ↑(Complex.arg x) - ↑(Complex.arg y)

@[simp]

theorem Complex.arg_coe_angle_toReal_eq_arg (z : ℂ) : Real.Angle.toReal ↑(Complex.arg z) = Complex.arg z

theorem Complex.arg_coe_angle_eq_iff_eq_toReal {z : ℂ} {θ : Real.Angle} : ↑(Complex.arg z) = θ ↔ Complex.arg z = Real.Angle.toReal θ

@[simp]

theorem Complex.arg_coe_angle_eq_iff {x : ℂ} {y : ℂ} : ↑(Complex.arg x) = ↑(Complex.arg y) ↔ Complex.arg x = Complex.arg y

theorem Complex.arg_mul_eq_add_arg_iff {x : ℂ} {y : ℂ} (hx₀ : x ≠ 0) (hy₀ : y ≠ 0) : Complex.arg (x * y) = Complex.arg x + Complex.arg y ↔ Complex.arg x + Complex.arg y ∈ Set.Ioc (-Real.pi) Real.pi

theorem Complex.arg_mul {x : ℂ} {y : ℂ} (hx₀ : x ≠ 0) (hy₀ : y ≠ 0) : Complex.arg x + Complex.arg y ∈ Set.Ioc (-Real.pi) Real.pi → Complex.arg (x * y) = Complex.arg x + Complex.arg y

Alias of the reverse direction of Complex.arg_mul_eq_add_arg_iff.

theorem Complex.mem_slitPlane_iff_arg {z : ℂ} : z ∈ Complex.slitPlane ↔ Complex.arg z ≠ Real.pi ∧ z ≠ 0

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 ∈ Complex.slitPlane) : Complex.arg z ≠ Real.pi

theorem Complex.arg_eq_nhds_of_re_pos {x : ℂ} (hx : 0 < x.re) : Complex.arg =ᶠ[nhds x] fun (x : ℂ) => Real.arcsin (x.im / Complex.abs x)

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 : ℂ) => Real.arcsin ((-x).im / Complex.abs x) + 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 : ℂ) => Real.arcsin ((-x).im / Complex.abs x) - Real.pi

theorem Complex.arg_eq_nhds_of_im_pos {z : ℂ} (hz : 0 < z.im) : Complex.arg =ᶠ[nhds z] fun (x : ℂ) => Real.arccos (x.re / Complex.abs x)

theorem Complex.arg_eq_nhds_of_im_neg {z : ℂ} (hz : z.im < 0) : Complex.arg =ᶠ[nhds z] fun (x : ℂ) => -Real.arccos (x.re / Complex.abs x)

theorem Complex.continuousAt_arg {x : ℂ} (h : x ∈ Complex.slitPlane) : ContinuousAt Complex.arg x

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}) (nhds (-Real.pi))

theorem Complex.continuousWithinAt_arg_of_re_neg_of_im_zero {z : ℂ} (hre : z.re < 0) (him : z.im = 0) : ContinuousWithinAt Complex.arg {z : ℂ | 0 ≤ z.im} z

theorem Complex.tendsto_arg_nhdsWithin_im_nonneg_of_re_neg_of_im_zero {z : ℂ} (hre : z.re < 0) (him : z.im = 0) : Filter.Tendsto Complex.arg (nhdsWithin z {z : ℂ | 0 ≤ z.im}) (nhds Real.pi)

theorem Complex.continuousAt_arg_coe_angle {x : ℂ} (h : x ≠ 0) : ContinuousAt (Real.Angle.coe ∘ Complex.arg) x