no goals
α : Type ?u.72258
β : Type ?u.72261
n d k N : ℕ
x : Fin n → ℕ
a : Fin (n + 1) → ℕ
⊢ ↑(map d) a = a 0 + (∑ x : Fin n, a (Fin.succ x) * d ^ ↑x) * d
simp [map, Fin.sum_univ_succ, _root_.pow_succ', ← mul_assoc, ← sum_mul]