arg_zpow_coe_angle — Mathlib

English

For any x ≠ 0, arg(-x) = arg x + π; and more generally arg(conj x) = - arg x.

Русский

Для x ≠ 0, arg(-x) = arg x + π; и в общем случае arg(conj x) = - arg x.

LaTeX

$$$\\\\arg(\\\\overline{x}) = -\\\\arg x \\\\text{ (as Real.Angle)}$$$

Lean4

theorem arg_zpow_coe_angle (x : ℂ) (n : ℤ) : (arg (x ^ n) : Real.Angle) = n • (arg x : Real.Angle) := by
  match n with
  | Int.ofNat m => simp [arg_pow_coe_angle]
  | Int.negSucc m => simp [arg_pow_coe_angle]

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