English
If f1 and f2 are polynomials with total degree sum less than |σ|, then the number of common zeros of (f1,f2) is divisible by p.
Русский
Если два многочлена имеют суммарную степень меньше количества переменных, то число общих нулей делимо на p.
LaTeX
$$$p \\mid |\\{x\\mid f_1(x)=0 \\wedge f_2(x)=0\\}|$ when $deg(f_1)+deg(f_2) < |\\sigma|$.$$
Lean4
/-- 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`. -/
theorem char_dvd_card_solutions_of_fintype_sum_lt [Fintype ι] {f : ι → MvPolynomial σ K}
(h : (∑ i, (f i).totalDegree) < Fintype.card σ) : p ∣ Fintype.card { x : σ → K // ∀ i, eval x (f i) = 0 } := by
simpa using char_dvd_card_solutions_of_sum_lt p h
