no goals
σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Finite σ
p : MvPolynomial σ K
h : ∀ (v : σ → K), ↑(eval v) p = 0
hp : p ∈ restrictDegree σ K (Fintype.card K - 1)
p' : R σ K := { val := p, property := hp }
this : p' ∈ ker (evalᵢ σ K)
⊢ p' = 0
rwa [ker_evalₗ, mem_bot] at this