English
The argument of the conjugate satisfies arg(conj z) = if arg z = π then π else −arg z.
Русский
Аргумент сопряжённого числа: arg(conj z) = если arg z = π, то π, иначе −arg z.
LaTeX
$$$$ \arg(\overline{z}) = \begin{cases} \pi & \text{if } \arg z = \pi, \\ -\arg z & \text{otherwise}. \end{cases} $$$$
Lean4
theorem arg_conj (x : ℂ) : arg (conj x) = if arg x = π then π else -arg x :=
by
simp_rw [arg_eq_pi_iff, arg, neg_im, conj_im, conj_re, norm_conj, neg_div, neg_neg, Real.arcsin_neg]
rcases lt_trichotomy x.re 0 with (hr | hr | hr) <;> rcases lt_trichotomy x.im 0 with (hi | hi | hi)
· simp [hr, hr.not_ge, hi.le, hi.ne, not_le.2 hi, add_comm]
· simp [hr, hr.not_ge, hi]
· simp [hr, hr.not_ge, hi.ne.symm, hi.le, not_le.2 hi, sub_eq_neg_add]
· simp [hr]
· simp [hr]
· simp [hr]
· simp [hr.le, hi.ne]
· simp [hr.le, hr.le.not_gt]
· simp [hr.le, hr.le.not_gt]
