arg_mul_coe_angle — Mathlib

English

For nonzero x,y, arg(x/y) = arg x − arg y.

Русский

При ненулевых x, y аргумент x/y равен аргументу x минус аргумент y.

LaTeX

$$$\\\\arg\\\\left(\\\\frac{x}{y}\\\\right) = \\\\arg x - \\\\arg y$$$

Lean4

theorem arg_mul_coe_angle {x y : ℂ} (hx : x ≠ 0) (hy : y ≠ 0) : (arg (x * y) : Real.Angle) = arg x + arg y :=
  by
  convert
    arg_mul_cos_add_sin_mul_I_coe_angle (mul_pos (norm_pos_iff.mpr hx) (norm_pos_iff.mpr hy))
      (arg x + arg y : Real.Angle) using
    3
  simp_rw [← Real.Angle.coe_add, Real.Angle.sin_coe, Real.Angle.cos_coe, ofReal_cos, ofReal_sin, cos_add_sin_I,
    ofReal_add, add_mul, exp_add, ofReal_mul]
  rw [mul_assoc, mul_comm (exp _), ← mul_assoc (‖y‖ : ℂ), norm_mul_exp_arg_mul_I, mul_comm y, ← mul_assoc,
    norm_mul_exp_arg_mul_I]

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