angle_exp_one — Mathlib

English

For real x, the angle between exp(i x) and 1 equals the absolute value of the modular expression of x.

Русский

Для действительного x угол между exp(i x) и 1 равен модулю некотоrого модулярного выражения от x.

LaTeX

$$$$\angle\left(\exp(i x), 1\right) = \left| \operatorname{toIocMod}(2\pi_{pos})(-\pi) x \right|.$$$$

Lean4

theorem angle_exp_one (x : ℝ) : angle (exp (x * I)) 1 = |toIocMod Real.two_pi_pos (-π) x| := by
  simpa using angle_exp_exp x 0

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