Primitive additive-character infrastructure

The Fourier arguments in this development are run against a fixed primitive complex additive character of the finite field. Mathlib supplies one, so no choice principle beyond Mathlib's own construction is needed. This module also records the elementary fact that any primitive complex additive character is nonprincipal.

noncomputable def KasamiCyclicAdditive.primitiveAddChar (K : Type u_2) [Field K] [Fintype K] : AddChar K ℂ

Mathlib's canonical primitive complex additive character on a finite field.

Equations

• KasamiCyclicAdditive.primitiveAddChar K = AddChar.FiniteField.primitiveChar_to_Complex K

theorem KasamiCyclicAdditive.primitiveAddChar_isPrimitive {K : Type u_1} [Field K] [Fintype K] : (primitiveAddChar K).IsPrimitive

The canonical complex additive character is primitive.

theorem KasamiCyclicAdditive.ne_one_of_isPrimitive {K : Type u_1} [Field K] {psi : AddChar K ℂ} (hpsi : psi.IsPrimitive) : psi ≠ 1

A primitive additive character is not the principal character.