∀ {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 }