char_dvd_card_solutions
theorem char_dvd_card_solutions :
∀ {K : Type u_1} {σ : Type u_2} [inst : Fintype K] [inst_1 : Field K] [inst_2 : Fintype σ] [inst_3 : DecidableEq σ]
[inst_4 : DecidableEq K] (p : ℕ) [inst_5 : CharP K p] {f : MvPolynomial σ K},
f.totalDegree < Fintype.card σ → p ∣ Fintype.card { x // (MvPolynomial.eval x) f = 0 }
The Chevalley–Warning theorem, in its unary version, states the following: Given a finite field `K` of characteristic `p` and a finite set of variables `σ`, consider any multivariate polynomial `f` with variables from `σ` and coefficients from `K`. If the total degree of `f` is less than the number of elements in `σ`, then the number of solutions to the equation `f = 0` in `K` is a multiple of `p`. This theorem also asserts that the equality relation `=` on both `σ` and `K` is decidable. The theorem in its more general form allows a family of polynomials `f i`, and can be found as `char_dvd_card_solutions_of_sum_lt`.
More concisely: In a finite field `K` of characteristic `p`, if the total degree of a multivariate polynomial `f` with variables from a finite set `σ` and coefficients from `K` is less than the cardinality of `σ`, then the number of solutions to `f = 0` is a multiple of `p`. Additionally, the equality relation on both `σ` and `K` is decidable.
|
char_dvd_card_solutions_of_sum_lt
theorem char_dvd_card_solutions_of_sum_lt :
∀ {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 : ℕ) [inst_5 : CharP K p] {s : Finset ι}
{f : ι → MvPolynomial σ K},
(s.sum fun i => (f i).totalDegree) < Fintype.card σ →
p ∣ Fintype.card { x // ∀ i ∈ s, (MvPolynomial.eval x) (f i) = 0 }
The **Chevalley–Warning theorem** in its finitary version is stated as follows:
Given a finite field `K` of characteristic `p`, and `σ` and `ι` as finite types, consider `f` as a finite family of multivariate polynomials in finitely many variables (`X s`, `s : σ`) over the field `K`. Each polynomial in the family is indexed by `ι`. If the sum of the total degrees of the polynomials is less than the number of elements in `σ`, then the number of common solutions of the polynomials (i.e., the solutions that satisfy all the polynomials in the family) is divisible by `p`. The divisibility is expressed as `p` divides `Fintype.card {x // ∀ i ∈ s, (MvPolynomial.eval x) (f i) = 0}`, where `Fintype.card` gives the number of elements and `{x // ∀ i ∈ s, (MvPolynomial.eval x) (f i) = 0}` represents the set of common solutions.
More concisely: If `K` is a finite field of characteristic `p`, and `f` is a finite family of multivariate polynomials over `K` whose total degrees are less than the number of variables, then the number of common solutions of the polynomials is a multiple of `p`.
|
char_dvd_card_solutions_of_add_lt
theorem char_dvd_card_solutions_of_add_lt :
∀ {K : Type u_1} {σ : Type u_2} [inst : Fintype K] [inst_1 : Field K] [inst_2 : Fintype σ] [inst_3 : DecidableEq σ]
[inst_4 : DecidableEq K] (p : ℕ) [inst_5 : CharP K p] {f₁ f₂ : MvPolynomial σ K},
f₁.totalDegree + f₂.totalDegree < Fintype.card σ →
p ∣ Fintype.card { x // (MvPolynomial.eval x) f₁ = 0 ∧ (MvPolynomial.eval x) f₂ = 0 }
The binary version of the **Chevalley–Warning theorem** states that, given two multivariate polynomials `f₁` and `f₂` in a finite number of variables (`X s`, `s : σ`) over a finite field of characteristic `p`, if the sum of the total degrees of `f₁` and `f₂` is less than the cardinality of `σ`, then the number of common solutions of `f₁` and `f₂` is divisible by `p`. In other words, given a field `K` of characteristic `p` and a finite type `σ`, if `f₁` and `f₂` are two multivariate polynomials in variables from `σ` over `K`, and if the sum of their total degrees is less than the number of elements in `σ`, then the cardinality of the set of common zeros of `f₁` and `f₂` is a multiple of `p`.
More concisely: Given multivariate polynomials `f₁` and `f₂` over a finite field `K` of characteristic `p` with finite type `σ`, if the total degrees of `f₁` and `f₂` sum to less than the cardinality of `σ`, then the number of common zeros of `f₁` and `f₂` is a multiple of `p`.
|
char_dvd_card_solutions_of_fintype_sum_lt
theorem char_dvd_card_solutions_of_fintype_sum_lt :
∀ {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 : ℕ) [inst_5 : CharP K p] [inst_6 : Fintype ι]
{f : ι → MvPolynomial σ K},
(Finset.univ.sum fun i => (f i).totalDegree) < Fintype.card σ →
p ∣ Fintype.card { x // ∀ (i : ι), (MvPolynomial.eval x) (f i) = 0 }
The Chevalley–Warning theorem in its Fintype version states a property about simultaneous solutions of polynomial equations over a finite field. Specifically, let `K` be a finite field of characteristic `p`, `σ` a set of variables, and `ι` an index set. Consider a family `f : ι → MvPolynomial σ K` of multivariate polynomials over `K` in variables `σ`. If the sum of the total degrees of these polynomials is less than the number of elements in `σ`, then the number of common solutions of these polynomials is divisible by `p`. These solutions are elements `x : σ → K` such that each polynomial `f i`, for `i` in `ι`, evaluates to zero under `x`.
More concisely: If `K` is a finite field of characteristic `p`, `σ` a set of variables, `ι` an index set, and `f : ι → MvPolynomial σ K` a family of multivariate polynomials over `K` in variables `σ` with total degree less than the cardinality of `σ`, then the number of common solutions of these polynomials is a multiple of `p`.
|