Additive characters valued in the unit circle #
This file defines additive characters, valued in the unit circle, from either
- the ring
ZMod Nfor any non-zero naturalN, - the additive circle
ℝ / T ⬝ ℤ, for any realT.
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 #
The additive character from ZMod N to the unit circle in ℂ, sending j mod N to
exp (2 * π * I * j / 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.
The additive character from ZMod N to ℂ, sending j mod N to exp (2 * π * I * j / N).
The standard additive character ZMod N → ℂ is primitive.
ZMod.toCircle as an AddChar into rootsOfUnity n Circle.
Equations
- ZMod.rootsOfUnityAddChar n = { toFun := fun (x : ZMod n) => ⟨toUnits (ZMod.toCircle x), ⋯⟩, map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ }
Interpret n-th roots of unity in ℂ as elements of the circle
Equations
- rootsOfUnitytoCircle n = { toFun := fun (z : ↥(rootsOfUnity n ℂ)) => ⟨↑↑z, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }
Equivalence of the nth roots of unity of the Circle with nth roots of unity of the complex numbers
Equations
- One or more equations did not get rendered due to their size.