no goals
p : ℕ
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : DecidableEq R
S : Type ?u.129330
inst✝² : CommRing S
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ℕ → A
n : ℕ
⊢ ↑(aeval f) (W_ R n) = ∑ i in range (n + 1), ↑p ^ i * f i ^ p ^ (n - i)
simp [wittPolynomial, AlgHom.map_sum, aeval_monomial, Finsupp.prod_single_index]