English
The unary Chevalley–Warning theorem reduces to the finite-type version; the vanishing counts hold in the finite setting.
Русский
Унарная версия теоремы Чевалле-Уорнинга сводится к версии для конечного множества переменных.
LaTeX
$$$\\text{char\_dvd\_card\_solutions\_of\_fintype\_sum\_lt}$ applies to the unary case with p dividing the count.$$
Lean4
/-- The **Chevalley–Warning theorem**, unary version.
Let `f` be a multivariate polynomial in finitely many variables (`X s`, `s : σ`)
over a finite field of characteristic `p`.
Assume that the total degree of `f` is less than the cardinality of `σ`.
Then the number of solutions of `f` is divisible by `p`.
See `char_dvd_card_solutions_of_sum_lt` for a version that takes a family of polynomials `f i`. -/
theorem char_dvd_card_solutions {f : MvPolynomial σ K} (h : f.totalDegree < Fintype.card σ) :
p ∣ Fintype.card { x : σ → K // eval x f = 0 } :=
by
let F : Unit → MvPolynomial σ K := fun _ => f
have : (∑ i : Unit, (F i).totalDegree) < Fintype.card σ := h
convert char_dvd_card_solutions_of_sum_lt p this
aesop
