K : Type u_2
σ : Type u_1
ι : Type ?u.683318
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
f₁ f₂ : MvPolynomial σ K
h : totalDegree f₁ + totalDegree f₂ < Fintype.card σ
F : Bool → MvPolynomial σ K := fun b => bif b then f₂ else f₁
⊢ p ∣ Fintype.card { x // ↑(eval x) f₁ = 0 ∧ ↑(eval x) f₂ = 0 }
K : Type u_2
σ : Type u_1
ι : Type ?u.683318
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
f₁ f₂ : MvPolynomial σ K
h : totalDegree f₁ + totalDegree f₂ < Fintype.card σ
⊢ p ∣ Fintype.card { x // ↑(eval x) f₁ = 0 ∧ ↑(eval x) f₂ = 0 }
let F : Bool → MvPolynomial σ K := fun b => cond b f₂ f₁
K : Type u_2
σ : Type u_1
ι : Type ?u.683318
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
f₁ f₂ : MvPolynomial σ K
h : totalDegree f₁ + totalDegree f₂ < Fintype.card σ
F : Bool → MvPolynomial σ K := fun b => bif b then f₂ else f₁
this : ∑ b : Bool, totalDegree (F b) < Fintype.card σ
⊢ p ∣ Fintype.card { x // ↑(eval x) f₁ = 0 ∧ ↑(eval x) f₂ = 0 }
K : Type u_2
σ : Type u_1
ι : Type ?u.683318
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
f₁ f₂ : MvPolynomial σ K
h : totalDegree f₁ + totalDegree f₂ < Fintype.card σ
F : Bool → MvPolynomial σ K := fun b => bif b then f₂ else f₁
⊢ p ∣ Fintype.card { x // ↑(eval x) f₁ = 0 ∧ ↑(eval x) f₂ = 0 }
have : (∑ b : Bool, (F b).totalDegree) < Fintype.card σ := (add_comm _ _).trans_lt h
no goals
K : Type u_2
σ : Type u_1
ι : Type ?u.683318
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
f₁ f₂ : MvPolynomial σ K
h : totalDegree f₁ + totalDegree f₂ < Fintype.card σ
F : Bool → MvPolynomial σ K := fun b => bif b then f₂ else f₁
this : ∑ b : Bool, totalDegree (F b) < Fintype.card σ
⊢ p ∣ Fintype.card { x // ↑(eval x) f₁ = 0 ∧ ↑(eval x) f₂ = 0 }
simpa only [Bool.forall_bool] using char_dvd_card_solutions_of_fintype_sum_lt p this