# The Chevalley–Warning theorem #

This file contains a proof of the Chevalley–Warning theorem.
Throughout most of this file, `K`

denotes a finite field
and `q`

is notation for the cardinality of `K`

.

## Main results #

- Let
`f`

be a multivariate polynomial in finitely many variables (`X s`

,`s : σ`

) such that the total degree of`f`

is less than`(q-1)`

times the cardinality of`σ`

. Then the evaluation of`f`

on all points of`σ → K`

(aka`K^σ`

) sums to`0`

. (`sum_eval_eq_zero`

) - The Chevalley–Warning theorem (
`char_dvd_card_solutions_of_sum_lt`

). Let`f i`

be a finite family of multivariate polynomials in finitely many variables (`X s`

,`s : σ`

) such that the sum of the total degrees of the`f i`

is less than the cardinality of`σ`

. Then the number of common solutions of the`f i`

is divisible by the characteristic of`K`

.

## Notation #

`K`

is a finite field`q`

is notation for the cardinality of`K`

`σ`

is the indexing type for the variables of a multivariate polynomial ring over`K`

The **Chevalley–Warning theorem**, finitary version.
Let `(f i)`

be a finite family of multivariate polynomials
in finitely many variables (`X s`

, `s : σ`

) over a finite field of characteristic `p`

.
Assume that the sum of the total degrees of the `f i`

is less than the cardinality of `σ`

.
Then the number of common solutions of the `f i`

is divisible by `p`

.

The **Chevalley–Warning theorem**, `Fintype`

version.
Let `(f i)`

be a finite family of multivariate polynomials
in finitely many variables (`X s`

, `s : σ`

) over a finite field of characteristic `p`

.
Assume that the sum of the total degrees of the `f i`

is less than the cardinality of `σ`

.
Then the number of common solutions of the `f i`

is divisible by `p`

.

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`

.

The **Chevalley–Warning theorem**, binary version.
Let `f₁`

, `f₂`

be two multivariate polynomials in finitely many variables (`X s`

, `s : σ`

) over a
finite field of characteristic `p`

.
Assume that the sum of the total degrees of `f₁`

and `f₂`

is less than the cardinality of `σ`

.
Then the number of common solutions of the `f₁`

and `f₂`

is divisible by `p`

.