arg_of_im_nonneg_of_ne_zero — Mathlib

English

If Re(z) < 0 and Im(z) ≥ 0, then arg z = arcsin((-z).im / ||z||) + π.

Русский

Если Re(z) < 0 и Im(z) ≥ 0, то arg z = arcsin((-z).Im / ||z||) + π.

LaTeX

$$$$ \arg z = \operatorname{arcsin}\left( \frac{(-z).im}{\|z\|} \right) + \pi, \quad \text{ если } \operatorname{Re}(z) < 0, \operatorname{Im}(z) \ge 0. $$$$

Lean4

theorem arg_of_im_nonneg_of_ne_zero {z : ℂ} (h₁ : 0 ≤ z.im) (h₂ : z ≠ 0) : arg z = Real.arccos (z.re / ‖z‖) := by
  rw [← cos_arg h₂, Real.arccos_cos (arg_nonneg_iff.2 h₁) (arg_le_pi _)]

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