toCircle_intCast — Mathlib

English

For any integer j, the additive character evaluated at j mod N equals exp(2π i j / N).

Русский

Для целого j отображение z mod N даёт exp(2π i j / N).

LaTeX

$$$\\forall j \\in \\mathbb{Z},\\; toCircle(j \\bmod N) = \\exp\\left(2\\pi i \\frac{j}{N}\\right)$$$

Lean4

theorem toCircle_intCast (j : ℤ) : toCircle (j : ZMod N) = exp (2 * π * I * j / N) :=
  by
  rw [toCircle, AddChar.compAddMonoidHom_apply, toCircle_addChar, AddChar.coe_mk, AddCircle.toCircle,
    toAddCircle_intCast, Function.Periodic.lift_coe, Circle.coe_exp]
  push_cast
  ring_nf

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