English
If x ≠ 0, then (arg(-x) : Real.Angle) = arg x + π.
Русский
Если x ≠ 0, то (arg(-x)) = arg x + π.
LaTeX
$$$\\forall x \\, (x \\neq 0) \\\\Rightarrow \\\\operatorname{arg}(-x) = \\\\operatorname{arg} x + \\\\pi$$$
Lean4
theorem arg_neg_coe_angle {x : ℂ} (hx : x ≠ 0) : (arg (-x) : Real.Angle) = arg x + π :=
by
rcases lt_trichotomy x.im 0 with (hi | hi | hi)
· rw [arg_neg_eq_arg_add_pi_of_im_neg hi, Real.Angle.coe_add]
· 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, ← Real.Angle.coe_add, ←
two_mul, Real.Angle.coe_two_pi, Real.Angle.coe_zero]
· exact False.elim (hx (ext hr hi))
·
rw [arg_ofReal_of_nonneg hr.le, ← ofReal_neg, arg_ofReal_of_neg (Left.neg_neg_iff.2 hr), Real.Angle.coe_zero,
zero_add]
· rw [arg_neg_eq_arg_sub_pi_of_im_pos hi, Real.Angle.coe_sub, Real.Angle.sub_coe_pi_eq_add_coe_pi]
