arg_eq_zero_iff — Mathlib

English

Arg z = 0 iff the real part is nonnegative and the imaginary part is zero.

Русский

Arg z = 0 тогда и только тогда, когда действительная часть неотрицательна, а мнимая часть равна нулю.

LaTeX

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

Lean4

theorem arg_eq_zero_iff {z : ℂ} : arg z = 0 ↔ 0 ≤ z.re ∧ z.im = 0 :=
  by
  refine ⟨fun h => ?_, ?_⟩
  · rw [← norm_mul_cos_add_sin_mul_I z, h]
    simp [norm_nonneg]
  · obtain ⟨x, y⟩ := z
    rintro ⟨h, rfl : y = 0⟩
    exact arg_ofReal_of_nonneg h

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