tan_arg — Mathlib

English

For a nonzero complex number z, tan(arg z) equals Im(z) divided by Re(z).

Русский

Для нескалярного числа z: tan(arg z) = Im(z) / Re(z).

LaTeX

$$$$ \operatorname{tan}(\arg z) = \frac{\operatorname{Im}(z)}{\operatorname{Re}(z)}, \quad z \neq 0. $$$$

Lean4

@[simp]
theorem tan_arg (x : ℂ) : Real.tan (arg x) = x.im / x.re :=
  by
  by_cases h : x = 0
  · simp only [h, zero_div, Complex.zero_im, Complex.arg_zero, Real.tan_zero, Complex.zero_re]
  rw [Real.tan_eq_sin_div_cos, sin_arg, cos_arg h, div_div_div_cancel_right₀ (norm_ne_zero_iff.mpr h)]

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