Zulip Chat Archive

Stream: Is there code for X?

Topic: Sums over finsets and fintypes


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Mar 24 2021 at 11:39):

that's probably nat_cast_hom.map_sum

view this post on Zulip 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

view this post on Zulip 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:

view this post on Zulip Eric Wieser (Apr 02 2021 at 12:03):

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

view this post on Zulip Eric Wieser (Apr 02 2021 at 12:03):

At least, that was my claim

view this post on Zulip Gabriel Moise (Apr 02 2021 at 12:22):

Oh, I see, thank you!


Last updated: May 16 2021 at 05:21 UTC