Sums over finsets and fintypes

Stream: Is there code for X?

[Gabriel Moise]

Is there a way to prove this elegantly?

import linear_algebra.matrix

open_locale big_operators

universe u
variables {V : Type u} [fintype V]

lemma sum_coe_nat (F : V → ℕ) : ↑ (∑ x : V, F x) = ∑ x : V, (F x : ℤ) :=
begin
  sorry
end

[Kevin Buzzard]

There's a lemma in the library saying that finite sums commute with an additive group homomorphism so you could rewrite the statement so that it deals with an add monoid hom and then apply that

[Kevin Buzzard]

I don't know the name of the add_monoid_hom whose underlying function is the coercion though

[Eric Wieser]

that's probably nat_cast_hom.map_sum

[Eric Wieser]

Ah, it's int.of_nat_hom.map_sum _ _. I guess there are two different casts from nat to int, docs#nat.cast_ring_hom and docs#int.of_nat_hom

[Gabriel Moise]

I don't really see how I can use those 2 to prove my lemma right now, can you elaborate a little more? :smile:

[Eric Wieser]

int.of_nat_hom.map_sum _ _ is literally the entire proof

[Eric Wieser]

At least, that was my claim

[Gabriel Moise]

Oh, I see, thank you!