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
Instances For

    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
    Instances For
      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.

      theorem ZMod.toCircle_eq_circleExp {N : } [NeZero N] (j : ZMod N) :
      toCircle j = Circle.exp (2 * Real.pi * (j.val / N))
      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
      Instances For
        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) :

        The standard additive character ZMod N → ℂ is primitive.

        noncomputable def ZMod.rootsOfUnityAddChar (n : ) [NeZero n] :

        ZMod.toCircle as an AddChar into rootsOfUnity n Circle.

        Equations
        Instances For
          @[simp]
          theorem ZMod.rootsOfUnityAddChar_val (n : ) [NeZero n] (x : ZMod n) :
          noncomputable def rootsOfUnitytoCircle (n : ) [NeZero n] :

          Interpret n-th roots of unity in as elements of the circle

          Equations
          Instances For
            noncomputable def rootsOfUnityCircleEquiv (n : ) [NeZero n] :

            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.
            Instances For
              @[simp]
              theorem rootsOfUnityCircleEquiv_apply (n : ) [NeZero n] (w : (rootsOfUnity n Circle)) :
              ((rootsOfUnityCircleEquiv n) w) = w