no goals
α : Type u
β : Type u_1
inst✝¹ : Semiring α
inst✝ : Semiring β
x y : α
n : ℕ
f : α →+* β
⊢ ↑f (∑ i in range n, x ^ i * y ^ (n - 1 - i)) = ∑ i in range n, ↑f x ^ i * ↑f y ^ (n - 1 - i)
simp [f.map_sum]