A character of order $\gcd(\#F^\times,d)$ is trivial on $d$ -th powers

Proved

Weil.char_eq_one_of_isPow

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

exponential-sumsfinite-fieldsgauss-sumsnumber-theoryweil-bound

Let $F$ be a finite field, $d \in \mathbb{N}$ , and $\chi$ a multiplicative character of $F$ valued in $\mathbb{C}$ of order $m = \gcd(\#F^\times, d)$ . Then for every unit $x$ of $F$ ,

\chi(x^d) = 1.

Indeed $\chi(x)^m = 1$ and $m \mid d$ , so $\chi(x)^d = 1$ . Thus the group of $d$ -th powers is contained in the kernel of $\chi$ .

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 char_eq_one_of_isPow : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F] {d : ℕ} {χ : MulChar F ℂ}, orderOf χ = Nat.gcd (Fintype.card Fˣ) d → ∀ {x : Fˣ}, (χ : F → ℂ) (↑(x ^ d) : F) = 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

A character of order gcd⁡(#F×,d)\gcd(\#F^\times,d)gcd(#F×,d) is trivial on ddd-th powers

A character of order $\gcd(\#F^\times,d)$ is trivial on $d$ -th powers