The Gauss sum of the trivial character equals $-1$

Proved

Weil.gaussSum_one_mulShift

by tabbott · Sep 2, 2026 · Mathlib c5ea003 (Lean v4.30.0)

exponential-sumsfinite-fieldsgauss-sumsnumber-theoryweil-bound

Let $F$ be a finite field, $\psi$ a non-trivial additive character of $F$ valued in $\mathbb{C}$ , and $a \in F$ with $a \ne 0$ . Writing $\psi_a$ for $x \mapsto \psi(ax)$ and $1$ for the trivial multiplicative character (which vanishes at $0$ and is $1$ on units),

g(1, \psi_a) = -1.

The complete sum $\sum_{u \in F}\psi(au)$ vanishes and the $u=0$ term contributes $1$ , so the sum over units is $-1$ . This is the $j = 0$ term that cancels the $x = 0$ contribution in the monomial decomposition.

Preamble

import Mathlib.NumberTheory.GaussSum
import Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
import Mathlib.NumberTheory.MulChar.Lemmas
import Mathlib.GroupTheory.SpecificGroups.Cyclic
import Mathlib.GroupTheory.Index
import Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
import Mathlib.Analysis.SpecialFunctions.Sqrt
import Mathlib.Analysis.RCLike.Basic
import Mathlib.Analysis.Complex.Basic
import Mathlib.Algebra.Field.GeomSum
import Mathlib.Algebra.Order.BigOperators.Group.Finset

set_option autoImplicit false
set_option linter.unusedSectionVars false
set_option linter.unusedVariables false

universe u_1 u_2

open AddChar MulChar Finset

Formal statement

namespace Weil
theorem gaussSum_one_mulShift : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [DecidableEq F] (ψ : AddChar F ℂ), ψ ≠ 1 → ∀ {a : F}, a ≠ 0 → gaussSum 1 (AddChar.mulShift ψ a) = -1 := by sorry
end Weil

Source

Ireland & Rosen, A Classical Introduction to Modern Number Theory, 2nd ed., Springer GTM 84, Ch. 8 (Gauss and Jacobi Sums)

View graph

The Gauss sum of the trivial character equals −1-1−1

The Gauss sum of the trivial character equals $-1$