arg_pow_coe_angle — Mathlib

English

For nonzero x, arg(-x) = arg x − π if Im x > 0; arg(-x) = arg x + π if Im x < 0; and arg(-x) = arg x if Im x = 0 and Re x ≥ 0, etc.

Русский

Для ненулевого x: если Im x > 0, то arg(-x) = arg x − π; если Im x < 0, то arg(-x) = arg x + π; если Im x = 0, то зависит от Re x.

LaTeX

$$$\\\\arg(-x) = \\\\arg x - \\\\pi \\\\iff \\\\Im x > 0 \\\\lor (\\\\Im x = 0 \\\\land \\\\Re x < 0)$$$

Lean4

theorem arg_pow_coe_angle (x : ℂ) (n : ℕ) : (arg (x ^ n) : Real.Angle) = n • (arg x : Real.Angle) :=
  by
  obtain rfl | x0 := eq_or_ne x 0
  · by_cases n0 : n = 0 <;> simp [n0]
  ·
    induction n with
    | zero => simp
    | succ n ih => rw [pow_succ, arg_mul_coe_angle (pow_ne_zero n x0) x0, ih, succ_nsmul]

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