## Stream: Is there code for X?

### Topic: finsupp.sum commutes with monoid_hom

#### Eric Wieser (Oct 12 2020 at 16:00):

Does this exist?

def finsupp.sum {α : Type} {β : Type} {γ : Type} {δ : Type}
(f : α →₀ β) (g : α → β → γ) (h : γ →+ δ) : h (f.sum g) = f.sum (λ a b, h (g a b)) := sorry


#### Eric Wieser (Oct 12 2020 at 16:12):

I can prove it as:

def monoid_hom.map_finsupp_sum {α : Type} {β : Type} {γ : Type} {δ : Type}
(f : α →₀ β) (g : α → β → γ) (h : γ →+ δ) : h (f.sum g) = f.sum (λ a b, h (g a b)) := begin
rw finsupp.sum,
rw h.map_sum,
set g2 := λ a b, h (g a b),
conv_lhs {
congr,
skip,
funext,
change g2 x (f x),
},
rw ←finsupp.sum,
end


#### Yury G. Kudryashov (Oct 12 2020 at 16:39):

lemma add_monoid_hom.map_finsupp_sum {α : Type} {β : Type} {γ : Type} {δ : Type}
(f : α →₀ β) (g : α → β → γ) (h : γ →+ δ) : h (f.sum g) = f.sum (λ a b, h (g a b)) :=
h.map_sum _ _


#### Yury G. Kudryashov (Oct 12 2020 at 16:40):

Or better

@[to_additive]
lemma monoid_hom.map_finsupp_prod {α β γ δ : Type*}
[has_zero β] [comm_monoid γ] [comm_monoid δ]
(f : α →₀ β) (g : α → β → γ) (h : γ →* δ) : h (f.prod g) = f.prod (λ a b, h (g a b)) :=
h.map_prod _ _


#### Yury G. Kudryashov (Oct 12 2020 at 16:41):

I failed to find it in data/finsupp/basic

#### Eric Wieser (Oct 12 2020 at 17:07):

Are you happy to PR those?

#### Yury G. Kudryashov (Oct 12 2020 at 17:22):

Feel free to PR. I won't have time for this (I mean, monitoring the status of the PR) today.

#### Heather Macbeth (Oct 12 2020 at 17:25):

That explains why all our favourite Canadians are online at once! @Frédéric Dupuis @Yury G. Kudryashov @Adam Topaz

Yeah

(I think so)

#4585

#### Eric Wieser (Oct 12 2020 at 19:48):

Not included is alg_hom.map_finsupp_prod and alg_hom.map_finsupp_sum because I'm not sure where to put them

#### Eric Wieser (Oct 13 2020 at 10:39):

^ Those are now done in #4603. It's annoying how when you extend a structure, you have to manually copy across all the lemmas about the base structure.