The gcd of the unit-group order with an exponent is positive

Proved

Weil.gcdDeg_pos

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}$ , $\gcd(\#F^\times, d) > 0$ . The unit group of a finite field is non-empty, so the gcd is positive even when $d = 0$ .

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 gcdDeg_pos : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F] (d : ℕ), 0 < Nat.gcd (Fintype.card Fˣ) d := by sorry
end Weil

Source

Lidl & Niederreiter, Finite Fields, 2nd ed., Cambridge, Ch. 5 (Exponential Sums), Theorems 5.4, 5.11, 5.15, 5.30, 5.38

View graph