Counting square roots with the quadratic character (complex form)

Proved

Weil.card_sqrts_complex

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

exponential-sumsfinite-fieldsgauss-sumsnumber-theoryweil-bound

Let $F$ be a finite field of characteristic $\ne 2$ and let $\chi_2 : F \to \mathbb{C}$ be its quadratic character composed with $\mathbb{Z} \hookrightarrow \mathbb{C}$ . For every $u \in F$ ,

\#\{x \in F : x^2 = u\} = \chi_2(u) + 1

as complex numbers. This is the form in which the count enters the evaluation of a quadratic exponential sum.

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_sqrts_complex : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F], ringChar F ≠ 2 → ∀ (u : F), (↑(Finset.card {x : F | x ^ 2 = u}) : ℂ) = (MulChar.ringHomComp (quadraticChar F) (Int.castRingHom ℂ) : F → ℂ) u + 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