toCircle_apply — Mathlib

English

The value of toCircle on any j ∈ ZMod N is equal to exp(2π i j.val / N).

Русский

Значение toCircle на любом j ∈ ZMod N равно exp(2π i j.val / N).

LaTeX

$$$toCircle(j) = \\exp\\left(2\\pi i \\frac{j.\\mathrm{val}}{N}\\right)$$$

Lean4

/-- Explicit formula for `toCircle j`. Note that this is "evil" because it uses `ZMod.val`. Where
possible, it is recommended to lift `j` to `ℤ` and use `toCircle_intCast` instead.
-/
theorem toCircle_apply (j : ZMod N) : toCircle j = exp (2 * π * I * j.val / N) := by
  rw [← toCircle_natCast, natCast_zmod_val]

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