abs_arg_inv — Mathlib

English

The absolute value of the argument is preserved under taking inverses: |arg(x^{-1})| = |arg x|.

Русский

Модуль аргумента сохраняется при взятии обратного: |arg(x^{-1})| = |arg x|.

LaTeX

$$$$ \left|\arg(x^{-1})\right| = |\arg x|, \quad x \in \mathbb{C}. $$$$

Lean4

@[simp]
theorem abs_arg_inv (x : ℂ) : |x⁻¹.arg| = |x.arg| := by rw [arg_inv];
  split_ifs <;>
    simp [*]
      -- TODO: Replace the next two lemmas by general facts about periodic functions

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