English
arg(-x) = arg x + π iff Im x < 0 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 \\\\Im x < 0 \\\\lor (\\\\Im x = 0 \\\\land 0 < \\\\Re x)$$$
Lean4
theorem arg_neg_eq_arg_add_pi_iff {x : ℂ} : arg (-x) = arg x + π ↔ x.im < 0 ∨ x.im = 0 ∧ 0 < x.re :=
by
rcases lt_trichotomy x.im 0 with (hi | hi | hi)
· simp [hi, arg_neg_eq_arg_add_pi_of_im_neg]
· 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.not_gt, ← two_mul, Real.pi_ne_zero]
· simp [hr, Real.pi_ne_zero.symm]
· rw [arg_ofReal_of_nonneg hr.le, ← ofReal_neg, arg_ofReal_of_neg (Left.neg_neg_iff.2 hr)]
simp [hr]
·
simp [hi, hi.ne.symm, hi.not_gt, arg_neg_eq_arg_sub_pi_of_im_pos, sub_eq_add_neg, ← add_eq_zero_iff_neg_eq,
Real.pi_ne_zero]
