arg_eq_pi_iff — Mathlib

English

Arg z = π iff z lies on the negative real axis (nonzero).

Русский

Arg z = π тогда и только тогда, когда z лежит на отрицательной вещественной оси (не ноль).

LaTeX

$$$$ \arg z = \pi \iff (\operatorname{Re}(z) < 0) \land (\operatorname{Im}(z) = 0). $$$$

Lean4

theorem arg_eq_pi_iff {z : ℂ} : arg z = π ↔ z.re < 0 ∧ z.im = 0 :=
  by
  by_cases h₀ : z = 0
  · simp [h₀, Real.pi_ne_zero.symm]
  constructor
  · intro h
    rw [← norm_mul_cos_add_sin_mul_I z, h]
    simp [h₀]
  · obtain ⟨x, y⟩ := z
    rintro ⟨h : x < 0, rfl : y = 0⟩
    rw [← arg_neg_one, ← arg_real_mul (-1) (neg_pos.2 h)]
    simp [← ofReal_def]

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