arg_eq_arg_iff — 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_eq_arg_iff {x y : ℂ} (hx : x ≠ 0) (hy : y ≠ 0) : arg x = arg y ↔ (‖y‖ / ‖x‖ : ℂ) * x = y :=
  by
  simp only [ext_norm_arg_iff, norm_mul, norm_div, norm_real, norm_norm, div_mul_cancel₀ _ (norm_ne_zero_iff.mpr hx),
    true_and]
  rw [← ofReal_div, arg_real_mul]
  exact div_pos (norm_pos_iff.mpr hy) (norm_pos_iff.mpr hx)

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