arg_inv — Mathlib

English

The argument of the inverse satisfies arg(x^{-1}) = if arg x = π then π else −arg x.

Русский

Аргумент обратного элемента: arg(x^{-1}) = если arg x = π, тогда π, иначе −arg x.

LaTeX

$$$$ \arg(x^{-1}) = \begin{cases} \pi & \text{если } \arg x = \pi, \\ -\arg x & \text{иначе}. \end{cases} $$$$

Lean4

theorem arg_inv (x : ℂ) : arg x⁻¹ = if arg x = π then π else -arg x :=
  by
  rw [← arg_conj, inv_def, mul_comm]
  by_cases hx : x = 0
  · simp [hx]
  · exact arg_real_mul (conj x) (by simp [hx])

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