Documentation

Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar

Additive characters valued in the unit circle #

This file defines additive characters, valued in the unit circle, from either

These results are separate from Analysis.SpecialFunctions.Complex.Circle in order to reduce the imports of that file.

The canonical map from the additive to the multiplicative circle, as an AddChar.

Equations

Additive characters valued in the complex circle #

noncomputable def ZMod.toCircle {N : } [NeZero N] :

The additive character from ZMod N to the unit circle in , sending j mod N to exp (2 * π * I * j / N).

Equations
theorem ZMod.toCircle_intCast {N : } [NeZero N] (j : ) :
(toCircle j) = Complex.exp (2 * Real.pi * Complex.I * j / N)
theorem ZMod.toCircle_natCast {N : } [NeZero N] (j : ) :
(toCircle j) = Complex.exp (2 * Real.pi * Complex.I * j / N)
theorem ZMod.toCircle_apply {N : } [NeZero N] (j : ZMod N) :
(toCircle j) = Complex.exp (2 * Real.pi * Complex.I * j.val / N)

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.

noncomputable def ZMod.stdAddChar {N : } [NeZero N] :

The additive character from ZMod N to , sending j mod N to exp (2 * π * I * j / N).

Equations
theorem ZMod.stdAddChar_coe {N : } [NeZero N] (j : ) :
stdAddChar j = Complex.exp (2 * Real.pi * Complex.I * j / N)
theorem ZMod.stdAddChar_apply {N : } [NeZero N] (j : ZMod N) :
stdAddChar j = (toCircle j)
theorem ZMod.isPrimitive_stdAddChar (N : ) [NeZero N] :
stdAddChar.IsPrimitive

The standard additive character ZMod N → ℂ is primitive.