toCircle — Mathlib

English

The canonical map from real numbers modulo T to the unit circle is given by exp(2π x / T).

Русский

Каноническое отображение от вещественных чисел по модулю T к единичной окружности задаётся как exp(2π x / T).

LaTeX

$$$$ \operatorname{toCircle}([x]) = \exp\left(\frac{2\pi}{T} x\right). $$$$

Lean4

/-- The canonical map `fun x => exp (2 π i x / T)` from `ℝ / ℤ • T` to the unit circle in `ℂ`.
If `T = 0` we understand this as the constant function 1. -/
noncomputable def toCircle : AddCircle T → Circle :=
  (@scaled_exp_map_periodic T).lift

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