arg_real_mul — Mathlib

English

For nonzero x,y, arg x = arg y iff y = (|y|/|x|) x.

Русский

Для ненулевых x,y: arg x = arg y тогда и только тогда, когда y = (|y|/|x|) x.

LaTeX

$$$x \\neq 0 \\land y \\neq 0 \\Rightarrow (\\\\arg x = \\\\arg y) \\\\Leftrightarrow y = \\\\frac{\\\\|y\\\\|}{\\\\|x\\\\|} x$$$

Lean4

theorem arg_real_mul (x : ℂ) {r : ℝ} (hr : 0 < r) : arg (r * x) = arg x :=
  by
  rcases eq_or_ne x 0 with (rfl | hx); · rw [mul_zero]
  conv_lhs =>
    rw [← norm_mul_cos_add_sin_mul_I x, ← mul_assoc, ← ofReal_mul,
      arg_mul_cos_add_sin_mul_I (mul_pos hr (norm_pos_iff.mpr hx)) x.arg_mem_Ioc]

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