Additive characters valued in the unit circle #
This file defines additive characters, valued in the unit circle, from either
- the ring
ZMod N
for 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' := ⋯ }
Instances For
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)
.
Instances For
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)
.
Instances For
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' := ⋯ }
Instances For
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' := ⋯ }
Instances For
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.