The modulus of a Gauss sum is $\sqrt{\#F}$

Proved

Weil.norm_gaussSum

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

exponential-sumsfinite-fieldsgauss-sumsnumber-theoryweil-bound

Square-root cancellation for Gauss sums. Let $F$ be a finite field, $\chi$ a non-trivial multiplicative character of $F$ valued in $\mathbb{C}$ , and $\psi$ a primitive additive character of $F$ . Then the Gauss sum $g(\chi,\psi)=\sum_{a\in F}\chi(a)\psi(a)$ has modulus exactly

\lVert g(\chi,\psi)\rVert = \sqrt{\#F}.

The sum has $\#F$ terms each of modulus at most $1$ , so the trivial bound is $\#F$ ; the content of the statement is that there is perfect square-root cancellation. This is the fundamental estimate underlying every Weil-type bound for complete exponential sums.

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 norm_gaussSum : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] (χ : MulChar F ℂ), χ ≠ 1 → ∀ (ψ : AddChar F ℂ), AddChar.IsPrimitive ψ → ‖gaussSum χ ψ‖ = √(↑(Fintype.card F) : ℝ) := 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 modulus of a Gauss sum is #F\sqrt{\#F}#F​

The modulus of a Gauss sum is $\sqrt{\#F}$