toCircle — Mathlib

English

From the additive character on ZMod N, one obtains a map to the unit circle, i.e., ZMod toCircle is a well-defined AddChar.

Русский

Из аддитивного символа на ZMod N получается отображение в единичную окружность.

LaTeX

$$$\\mathrm{toCircle} : AddChar(ZMod(N), Circle)$$$

Lean4

/-- The additive character from `ZMod N` to the unit circle in `ℂ`, sending `j mod N` to
`exp (2 * π * I * j / N)`. -/
noncomputable def toCircle : AddChar (ZMod N) Circle :=
  toCircle_addChar.compAddMonoidHom toAddCircle

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