no goals
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
hn : 0 < n
⊢ ↑(aeval (Function.uncurry fun i => ![].coeff)) (wittOne p n) = 0
simp only [hn, wittOne_pos_eq_zero, AlgHom.map_zero]