Theorems · Theorem · number theory

char_dvd_card_solutions_of_sum_lt

• 1000+ list: Chevalley–Warning theorem

∀ {K : Type u_1} {σ : Type u_2} {ι : Type u_3} [inst : Fintype K] [inst_1 : Field K] [inst_2 : Fintype σ]
  [inst_3 : DecidableEq σ] [inst_4 : DecidableEq K] (p : ℕ) [CharP K p] {s : Finset ι} {f : ι → MvPolynomial σ K},
  ∑ i ∈ s, (f i).totalDegree < Fintype.card σ → p ∣ Fintype.card { x // ∀ i ∈ s, (MvPolynomial.eval x) (f i) = 0 }

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.

Defined in

Mathlib.FieldTheory.ChevalleyWarning

Cited by

2 results in Mathlib

Foundations

Depth 144 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeFieldFintypeDecidableEqDecidableEqCharP