Passing coe through a sum

Stream: Is there code for X?

[Ethan Pronovost]

I'd like to pass the coe : $\N \to \Z$ through a finite sum

example (α : Type*) [fintype α] (f : α → ℕ) : ∑ x, (f x : ℤ) = int.of_nat (∑ x, f x) := sorry

I feel like this should be a one-liner but haven't gotten it to work. add_monoid_hom.map_finsum_of_injective seems promising. Any ideas on how to do this?

[Heather Macbeth]

@Ethan Pronovost You can do

import algebra.big_operators.basic

open_locale big_operators

example (α : Type*) [fintype α] (f : α → ℕ) : (∑ x, (f x : ℤ)) = int.of_nat (∑ x, f x) :=
(int.of_nat_hom.map_sum f _).symm

[Ethan Pronovost]

Thanks!