English
arg(-x) = arg x - π if and only if 0 < Im x or (Im x = 0 and Re x < 0).
Русский
arg(-x) = arg x - π тогда и только тогда, когда Im x > 0 или Im x = 0 и Re x < 0.
LaTeX
$$$\\\\arg(-x) = \\\\arg x - \\\\pi \\\\iff 0 < \\\\Im x \\\\lor (\\\\Im x = 0 \\\\land \\\\Re x < 0)$$$
Lean4
theorem arg_neg_eq_arg_sub_pi_iff {x : ℂ} : arg (-x) = arg x - π ↔ 0 < x.im ∨ x.im = 0 ∧ x.re < 0 :=
by
rcases lt_trichotomy x.im 0 with (hi | hi | hi)
·
simp [hi, hi.ne, hi.not_gt, arg_neg_eq_arg_add_pi_of_im_neg, sub_eq_add_neg, ← add_eq_zero_iff_eq_neg,
Real.pi_ne_zero]
· rw [(ext rfl hi : x = x.re)]
rcases lt_trichotomy x.re 0 with (hr | hr | hr)
· rw [arg_ofReal_of_neg hr, ← ofReal_neg, arg_ofReal_of_nonneg (Left.neg_pos_iff.2 hr).le]
simp [hr]
· simp [hr, Real.pi_ne_zero]
· rw [arg_ofReal_of_nonneg hr.le, ← ofReal_neg, arg_ofReal_of_neg (Left.neg_neg_iff.2 hr)]
simp [hr.not_gt, ← add_eq_zero_iff_eq_neg, Real.pi_ne_zero]
· simp [hi, arg_neg_eq_arg_sub_pi_of_im_pos]
