arg_mul_cos_add_sin_mul_I_sub — Mathlib

English

For any θ, arg(cos θ + i sin θ) equals θ modulo 2π, with an explicit representative.

Русский

Для любого θ арґумент cos θ + i sin θ равен θ по модулю 2π с явным представителем.

LaTeX

$$$\\\\arg(\\\\cos\\\\theta + i\\\\sin\\\\theta) = \\\\theta \\\\bmod 2\\\\pi$$$

Lean4

theorem arg_mul_cos_add_sin_mul_I_sub {r : ℝ} (hr : 0 < r) (θ : ℝ) :
    arg (r * (cos θ + sin θ * I)) - θ = 2 * π * ⌊(π - θ) / (2 * π)⌋ :=
  by
  rw [arg_mul_cos_add_sin_mul_I_eq_toIocMod hr, toIocMod_sub_self, toIocDiv_eq_neg_floor, zsmul_eq_mul]
  ring_nf

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