Documentation

Mathlib.NumberTheory.LegendreSymbol.Complex

Additive characters on finite fields #

We construct a primitive additive character on a finite field F with values in ℂ. This file is kept separate from Mathlib.NumberTheory.LegendreSymbol.AddCharacter to avoid importing the fundamental theorem of algebra and Bochner integral into that file.

source
noncomputable def AddChar.FiniteField.primitiveChar_to_Complex (F : Type u_1) [Field F] [Finite F] :
AddChar F ℂ

A primitive additive character on the finite field F with values in ℂ.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem AddChar.FiniteField.primitiveChar_to_Complex_isPrimitive (F : Type u_1) [Field F] [Finite F] :
    (primitiveChar_to_Complex F).IsPrimitive