arg_cos_add_sin_mul_I — Mathlib

English

For θ ∈ (-π, π), arg(cos θ + i sin θ) = θ.

Русский

Для θ ∈ (-π, π) аргумент косинуса θ плюс i синус θ равен θ.

LaTeX

$$$\\\\arg(\\\\cos\\\\theta + i\\\\sin\\\\theta) = \\\\theta , \\\\theta \\\\in (-\\\\pi, \\\\pi)$$$

Lean4

theorem arg_cos_add_sin_mul_I {θ : ℝ} (hθ : θ ∈ Set.Ioc (-π) π) : arg (cos θ + sin θ * I) = θ := by
  rw [← one_mul (_ + _), ← ofReal_one, arg_mul_cos_add_sin_mul_I zero_lt_one hθ]

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