arg_mul_cos_add_sin_mul_I_eq_toIocMod

English

For positive r and θ ∈ ℝ, arg(r (cos θ + i sin θ)) equals the representative of θ in (-π, π] modulo 2π.

Русский

При положительном r и θ ∈ ℝ arg(r (cos θ + i sin θ)) равно представителю θ в (-π, π] по модулю 2π.

LaTeX

$$$\\\\arg\\\\left(r(\\\\cos\\\\theta + i\\\\sin\\\\theta)\\\\right) = \\\\mathrm{toIocMod}(2\\\\pi, -\\\\pi, \\\\theta)$$$

Lean4

theorem arg_mul_cos_add_sin_mul_I_eq_toIocMod {r : ℝ} (hr : 0 < r) (θ : ℝ) :
    arg (r * (cos θ + sin θ * I)) = toIocMod Real.two_pi_pos (-π) θ :=
  by
  have hi : toIocMod Real.two_pi_pos (-π) θ ∈ Set.Ioc (-π) π :=
    by
    convert toIocMod_mem_Ioc _ _ θ
    ring
  convert arg_mul_cos_add_sin_mul_I hr hi using 3
  simp [toIocMod, cos_sub_int_mul_two_pi, sin_sub_int_mul_two_pi]

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