arg_exp_mul_I — Mathlib

English

The argument of e^{iθ} is θ reduced modulo 2π to lie in (-π, π].

Русский

Аргумент e^{iθ} равен θ, приведённому по модулю 2π в интервал (-π, π].

LaTeX

$$$\\\\arg\\\\left(e^{i\\\\theta}\\\\right) = \\\\mathrm{toIocMod}\\\\left(2\\\\pi, -\\\\pi, \\\\theta\\\\right)$$$

Lean4

theorem arg_exp_mul_I (θ : ℝ) : arg (exp (θ * I)) = toIocMod (mul_pos two_pos Real.pi_pos) (-π) θ :=
  by
  convert arg_cos_add_sin_mul_I (θ := toIocMod (mul_pos two_pos Real.pi_pos) (-π) θ) _ using 2
  ·
    rw [← exp_mul_I, eq_sub_of_add_eq <| toIocMod_add_toIocDiv_zsmul _ _ θ, ofReal_sub, ofReal_zsmul, ofReal_mul,
      ofReal_ofNat, exp_mul_I_periodic.sub_zsmul_eq]
  · convert toIocMod_mem_Ioc _ _ _
    ring

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