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
  • AddCircle.toCircle_addChar = { toFun := AddCircle.toCircle, map_zero_eq_one' := , map_add_eq_mul' := }

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
  • ZMod.toCircle = AddCircle.toCircle_addChar.compAddMonoidHom ZMod.toAddCircle
theorem ZMod.toCircle_intCast {N : } [NeZero N] (j : ) :
(ZMod.toCircle j) = Complex.exp (2 * Real.pi * Complex.I * j / N)
theorem ZMod.toCircle_natCast {N : } [NeZero N] (j : ) :
(ZMod.toCircle j) = Complex.exp (2 * Real.pi * Complex.I * j / N)
theorem ZMod.toCircle_apply {N : } [NeZero N] (j : ZMod N) :
(ZMod.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.

theorem ZMod.injective_toCircle {N : } [NeZero N] :
Function.Injective ZMod.toCircle
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 : ) :
ZMod.stdAddChar j = Complex.exp (2 * Real.pi * Complex.I * j / N)
theorem ZMod.stdAddChar_apply {N : } [NeZero N] (j : ZMod N) :
ZMod.stdAddChar j = (ZMod.toCircle j)
theorem ZMod.injective_stdAddChar {N : } [NeZero N] :
Function.Injective ZMod.stdAddChar
theorem ZMod.isPrimitive_stdAddChar (N : ) [NeZero N] :
ZMod.stdAddChar.IsPrimitive

The standard additive character ZMod N → ℂ is primitive.