K : Type u_2
σ : Type u_1
ι : Type ?u.638341
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
f : MvPolynomial σ K
h : totalDegree f < Fintype.card σ
F : Unit → MvPolynomial σ K := fun x => f
⊢ p ∣ Fintype.card { x // ↑(eval x) f = 0 }
K : Type u_2
σ : Type u_1
ι : Type ?u.638341
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
f : MvPolynomial σ K
h : totalDegree f < Fintype.card σ
⊢ p ∣ Fintype.card { x // ↑(eval x) f = 0 }
let F : Unit → MvPolynomial σ K := fun _ => f
K : Type u_2
σ : Type u_1
ι : Type ?u.638341
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
f : MvPolynomial σ K
h : totalDegree f < Fintype.card σ
F : Unit → MvPolynomial σ K := fun x => f
this : ∑ i : Unit, totalDegree (F i) < Fintype.card σ
⊢ p ∣ Fintype.card { x // ↑(eval x) f = 0 }
K : Type u_2
σ : Type u_1
ι : Type ?u.638341
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
f : MvPolynomial σ K
h : totalDegree f < Fintype.card σ
F : Unit → MvPolynomial σ K := fun x => f
⊢ p ∣ Fintype.card { x // ↑(eval x) f = 0 }
have : (∑ i : Unit, (F i).totalDegree) < Fintype.card σ := h
case h.e'_4.h.h.e'_2.h.a
K : Type u_2
σ : Type u_1
ι : Type ?u.638341
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
f : MvPolynomial σ K
h : totalDegree f < Fintype.card σ
F : Unit → MvPolynomial σ K := fun x => f
this : ∑ i : Unit, totalDegree (F i) < Fintype.card σ
x✝ : σ → K
⊢ ↑(eval x✝) f = 0 ↔ ∀ (i : Unit), i ∈ univ → ↑(eval x✝) (F i) = 0
K : Type u_2
σ : Type u_1
ι : Type ?u.638341
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
f : MvPolynomial σ K
h : totalDegree f < Fintype.card σ
F : Unit → MvPolynomial σ K := fun x => f
this : ∑ i : Unit, totalDegree (F i) < Fintype.card σ
⊢ p ∣ Fintype.card { x // ↑(eval x) f = 0 }
convert char_dvd_card_solutions_of_sum_lt p this
no goals
case h.e'_4.h.h.e'_2.h.a
K : Type u_2
σ : Type u_1
ι : Type ?u.638341
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
f : MvPolynomial σ K
h : totalDegree f < Fintype.card σ
F : Unit → MvPolynomial σ K := fun x => f
this : ∑ i : Unit, totalDegree (F i) < Fintype.card σ
x✝ : σ → K
⊢ ↑(eval x✝) f = 0 ↔ ∀ (i : Unit), i ∈ univ → ↑(eval x✝) (F i) = 0
aesop