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.

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.

theorem AddChar.FiniteField.primitiveChar_to_Complex_isPrimitive (F : Type u_1) [Field F] [Finite F] : (primitiveChar_to_Complex F).IsPrimitive