no goals
K : Type u_3
σ : Type u_2
ι : Type u_1
inst✝⁶ : Fintype K
inst✝⁵ : Field K
inst✝⁴ : Fintype σ
inst✝³ : DecidableEq σ
inst✝² : DecidableEq K
p : ℕ
inst✝¹ : CharP K p
inst✝ : Fintype ι
f : ι → MvPolynomial σ K
h : ∑ i : ι, totalDegree (f i) < Fintype.card σ
⊢ p ∣ Fintype.card { x // ∀ (i : ι), ↑(eval x) (f i) = 0 }
simpa using char_dvd_card_solutions_of_sum_lt p h