no goals
p : ℕ
R S : Type u
σ : Type ?u.653400
idx : Type ?u.653403
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
n : ℕ
⊢ ↑(bind₁ 0) (wittPolynomial p R n) = 0
rw [← aeval_eq_bind₁, aeval_zero, constantCoeff_wittPolynomial, RingHom.map_zero]