arg_cos_add_sin_mul_I_eq_toIocMod

English

For real θ, arg(cos θ + i sin θ) = θ modulo 2π, in the representative (-π, π].

Русский

Для вещественного θ аргумент cos θ + i sin θ равен θ по модулю 2π, представление (-π, π].

LaTeX

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

Lean4

theorem arg_cos_add_sin_mul_I_eq_toIocMod (θ : ℝ) : arg (cos θ + sin θ * I) = toIocMod Real.two_pi_pos (-π) θ := by
  rw [← one_mul (_ + _), ← ofReal_one, arg_mul_cos_add_sin_mul_I_eq_toIocMod zero_lt_one]

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