Prove2Me

Non-empty fibres of the dd-th power map in a cyclic group all have the same size

Proved
Weil.card_pow_fiber

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

exponential-sumsfinite-fieldsgauss-sumsnumber-theoryweil-bound

Let GG be a finite cyclic abelian group, d∈Nd \in \mathbb{N}, and y∈Gy \in G a dd-th power. Then

#{x∈G:xd=y}=gcd⁡(#G,d).\#\{x \in G : x^d = y\} = \gcd(\#G, d).

A non-empty fibre of a group homomorphism is a coset of its kernel, so it has exactly #ker⁡\#\ker elements; for the dd-th power map on a cyclic group of order nn that is gcd⁡(n,d)\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_fiber : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : Fintype G] [inst_2 : DecidableEq G] [IsCyclic G] (d : ℕ) {y : G}, (∃ (x : G), x ^ d = y) → Finset.card {x : G | x ^ d = y} = 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