Reduced monomials over a finite field are independent

Over a finite field K, monomials ∏ j, x j ^ e j whose exponents are all below Fintype.card K are distinct as functions on σ → K when their exponent vectors are distinct, and in fact linearly independent (FiniteField.linearIndependent_prod_pow), by the combinatorial Nullstellensatz. So a combination of such monomials that vanishes at every point has zero coefficients (FiniteField.eq_zero_of_forall_sum_mul_prod_pow_eq_zero).

Main results

• FiniteField.linearIndependent_prod_pow: distinct reduced monomials are linearly independent functions.
• FiniteField.eq_zero_of_forall_sum_mul_prod_pow_eq_zero: a vanishing combination of distinct reduced monomials has zero coefficients.

References

• Adapted from MassProduction/HighRate/Independence.lean in S. Schlesinger, Boolean circuit mass production formalization.

theorem FiniteField.linearIndependent_prod_pow {K : Type u_1} [Field K] [Fintype K] {ι : Type u_2} {σ : Type u_3} [Fintype σ] (e : ι → σ → ℕ) (he : Function.Injective e) (hlt : ∀ (i : ι) (j : σ), e i j < Fintype.card K) : LinearIndependent K fun (i : ι) (x : σ → K) => ∏ j : σ, x j ^ e i j

Monomials ∏ j, X j ^ e i j with distinct exponent vectors, all of whose exponents are below Fintype.card K, are linearly independent as functions on σ → K.

theorem FiniteField.eq_zero_of_forall_sum_mul_prod_pow_eq_zero {K : Type u_1} [Field K] [Fintype K] {σ : Type u_2} {T : Type u_3} [Fintype σ] [Fintype T] (e : T → σ → ℕ) (he : Function.Injective e) (hlt : ∀ (t : T) (v : σ), e t v < Fintype.card K) (C : T → K) (h : ∀ (x : σ → K), ∑ t : T, C t * ∏ v : σ, x v ^ e t v = 0) (t : T) : C t = 0

Reduced monomials are independent: over a finite field K, if a combination ∑ₜ Cₜ ∏ᵥ xᵥ ^ eₜᵥ of monomials with pairwise distinct exponent vectors, all exponents below |K|, vanishes at every point, then all coefficients vanish.