arg_mul_eq_add_arg_iff — Mathlib

English

Let x,y ∈ ℂ with x ≠ 0 and y ≠ 0. Then (arg(xy) = arg x + arg y) if and only if arg x + arg y lies in the interval (-π, π] (i.e. in Ioc(-π, π)).

Русский

Для комплексных x,y с x ≠ 0, y ≠ 0 верно: arg(xy) = arg x + arg y тогда и только тогда, когда arg x + arg y ∈ (-π, π].

LaTeX

$$$ (\operatorname{arg}(xy)) = \operatorname{arg} x + \operatorname{arg} y \;\Longleftrightarrow\; \operatorname{arg} x + \operatorname{arg} y \in (-\pi, \pi] $$$

Lean4

theorem arg_mul_eq_add_arg_iff {x y : ℂ} (hx₀ : x ≠ 0) (hy₀ : y ≠ 0) :
    (x * y).arg = x.arg + y.arg ↔ arg x + arg y ∈ Set.Ioc (-π) π := by
  rw [← arg_coe_angle_toReal_eq_arg, arg_mul_coe_angle hx₀ hy₀, ← Real.Angle.coe_add,
    Real.Angle.toReal_coe_eq_self_iff_mem_Ioc]

Похожие утверждения