Existence of a multiplicative character of order $\gcd(\#F^\times, d)$

Proved

Weil.exists_mulChar_orderOf_gcdDeg

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

exponential-sumsfinite-fieldsgauss-sumsnumber-theoryweil-bound

For a finite field $F$ and $d \in \mathbb{N}$ there exists a multiplicative character $\chi$ of $F$ valued in $\mathbb{C}$ of order exactly $\gcd(\#F^\times, d)$ . The character group of $F^\times$ is cyclic of order $\#F - 1$ , and $\mathbb{C}$ contains primitive roots of unity of every order.

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 exists_mulChar_orderOf_gcdDeg : ∀ {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 := 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

Existence of a multiplicative character of order gcd⁡(#F×,d)\gcd(\#F^\times, d)gcd(#F×,d)

Existence of a multiplicative character of order $\gcd(\#F^\times, d)$