Evaluating a polynomial of degree at most two

Proved

Weil.eval_of_natDegree_le_two

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

exponential-sumsfinite-fieldsgauss-sumsnumber-theoryweil-bound

Let $R$ be a commutative ring and $f \in R[X]$ with $\deg f \le 2$ . Then for every $x \in R$ ,

f(x) = f_2 x^2 + f_1 x + f_0,

where $f_i$ denotes the coefficient of $X^i$ in $f$ .

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 eval_of_natDegree_le_two : ∀ {R : Type u_1} [inst : CommRing R] (f : Polynomial R), Polynomial.natDegree f ≤ 2 → ∀ (x : R), Polynomial.eval x f = Polynomial.coeff f 2 * x ^ 2 + Polynomial.coeff f 1 * x + Polynomial.coeff f 0 := by sorry
end Weil

Source

Iwaniec & Kowalski, Analytic Number Theory, AMS Colloquium Publications 53, 2004, Ch. 11 (Sums over finite fields), §11.1-11.3

View graph