English
For two polynomials f1,f2 with total degree sum bound, the count of solutions of f1 = 0 and f2 = 0 is divisible by p for finite variables.
Русский
Для двух полиномов при конечных переменных число решений делимо на p.
LaTeX
$$$p \\mid |\\{x\\mid f_1(x)=0 \\land f_2(x)=0\\}|$ when $deg(f_1)+deg(f_2) < |\\sigma|$.$$
Lean4
/-- 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`. -/
theorem char_dvd_card_solutions_of_add_lt {f₁ f₂ : MvPolynomial σ K}
(h : f₁.totalDegree + f₂.totalDegree < Fintype.card σ) :
p ∣ Fintype.card { x : σ → K // eval x f₁ = 0 ∧ eval x f₂ = 0 } :=
by
let F : Bool → MvPolynomial σ K := fun b => cond b f₂ f₁
have : (∑ b : Bool, (F b).totalDegree) < Fintype.card σ := (add_comm _ _).trans_lt h
simpa only [Bool.forall_bool] using char_dvd_card_solutions_of_fintype_sum_lt p this
