The argument of a quotient

Mathlib computes the argument of a quotient only modulo 2π (Complex.arg_div_coe_angle), and of a product exactly when the sum of the arguments lies in (-π, π] (Complex.arg_mul_eq_add_arg_iff). This file records the analogue for quotients, and its most common instance: for two points of the open upper half-plane the arguments lie in (0, π), so the argument of their quotient is the difference of their arguments.

Main results

• Complex.arg_div_eq_sub_arg_iff: arg (x / y) = arg x - arg y exactly when arg x - arg y ∈ (-π, π].
• Complex.arg_div_of_im_pos: if 0 < x.im and 0 < y.im, then arg (x / y) = arg x - arg y.

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

The argument of a quotient is the difference of the arguments exactly when that difference lies in (-π, π].

theorem Complex.arg_div_of_im_pos {x y : ℂ} (hx : 0 < x.im) (hy : 0 < y.im) : (x / y).arg = x.arg - y.arg

The argument of the quotient of two points of the open upper half-plane is the difference of their arguments.