The number of $d$ -th roots of unity in a finite cyclic group

Proved

Weil.card_pow_eq_one

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

exponential-sumsfinite-fieldsgauss-sumsnumber-theoryweil-bound

Let $G$ be a finite cyclic abelian group and $d \in \mathbb{N}$ . Then

\#\{x \in G : x^d = 1\} = \gcd(\#G, d).

The solutions form the kernel of the $d$ -th power endomorphism, which in a cyclic group of order $n$ has order $\gcd(n,d)$ .

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 card_pow_eq_one : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : Fintype G] [inst_2 : DecidableEq G] [IsCyclic G] (d : ℕ), Finset.card {x : G | x ^ d = 1} = Nat.gcd (Nat.card G) 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

The number of ddd-th roots of unity in a finite cyclic group

The number of $d$ -th roots of unity in a finite cyclic group