## Stream: Is there code for X?

### Topic: Sums over finsets and fintypes

#### Gabriel Moise (Mar 24 2021 at 10:52):

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 (Mar 24 2021 at 11:17):

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 (Mar 24 2021 at 11:29):

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

#### Eric Wieser (Mar 24 2021 at 11:39):

that's probably nat_cast_hom.map_sum

#### Eric Wieser (Mar 24 2021 at 11:41):

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 (Apr 02 2021 at 11:26):

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 (Apr 02 2021 at 12:03):

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

#### Eric Wieser (Apr 02 2021 at 12:03):

At least, that was my claim

#### Gabriel Moise (Apr 02 2021 at 12:22):

Oh, I see, thank you!

Last updated: May 16 2021 at 05:21 UTC