arg_mul_cos_add_sin_mul_I_coe_angle

English

For any x ∈ ℂ and natural n, arg(x^n) = n · arg(x).

Русский

Для любого x ∈ ℂ и натурального n арґумент x^n равен n · арґументу x.

LaTeX

$$$\\\\arg(x^n) = n \\\\cdot \\\\arg(x)$$$

Lean4

theorem arg_mul_cos_add_sin_mul_I_coe_angle {r : ℝ} (hr : 0 < r) (θ : Real.Angle) :
    (arg (r * (Real.Angle.cos θ + Real.Angle.sin θ * I)) : Real.Angle) = θ :=
  by
  induction θ using Real.Angle.induction_on with
  | _ θ
  rw [Real.Angle.cos_coe, Real.Angle.sin_coe, Real.Angle.angle_eq_iff_two_pi_dvd_sub]
  use ⌊(π - θ) / (2 * π)⌋
  exact mod_cast arg_mul_cos_add_sin_mul_I_sub hr θ

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