English
Let n be a positive integer. For every x in ZMod n there is a circle-valued character χ_x: ZMod n → Circle defined by χ_x(y) = exp(2π i x y / n). The collection {χ_x} (as x runs over ZMod n) yields all complex-valued additive characters of ZMod n; in particular the map x ↦ χ_x is injective.
Русский
Пусть n ∈ ℕ+, для каждого x ∈ ℤ/nℤ существует круговой символ χ_x: ℤ/nℤ → Circle, заданный χ_x(y) = exp(2π i x y / n). множество χ_x при x ∈ ℤ/nℤ образуют все комплекснозначные аддитивные символы ZMod n; в частности отображение x ↦ χ_x инъективно.
LaTeX
$$$ zmod(n)\, x\, y = \exp\left( 2 \pi i \frac{x y}{n} \right) $$$
Lean4
/-- Indexing of the complex characters of `ZMod n`. `AddChar.zmod n x` is the character sending `y`
to `e ^ (2 * π * i * x * y / n)`. -/
def zmod (x : ZMod n) : AddChar (ZMod n) Circle :=
AddChar.compAddMonoidHom ⟨AddCircle.toCircle, AddCircle.toCircle_zero, AddCircle.toCircle_add⟩ <|
ZMod.toAddCircle.comp <| .mulLeft x
