# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: Sum is linear

#### Oliver Nash (Mar 05 2021 at 20:47):

I'm a bit surprised that I can't find the following lemma anywhere:

```
import data.finsupp.basic
variables {α R M N : Type*}
variables [semiring R] [add_comm_monoid M] [semimodule R M] [add_comm_monoid N] [semimodule R N]
variables {f : α →₀ M} {g : α → M → N}
-- TODO Convenient coercion to state using `g : α → M →[R] N` instead of the unbundled hypothesis ?
@[simp] lemma finsupp.smul_sum' (h : ∀ (t : R) a m, g a (t • m) = t • g a m) (t : R) :
(t • f).sum g = t • (f.sum g) := sorry
```

I have a (horrid) proof that I can tidy up and push but I thought I'd check here first. Any ideas?

#### Adam Topaz (Mar 05 2021 at 20:50):

Isn't it possible to make docs#finsupp.smul_sum work here?

#### Oliver Nash (Mar 05 2021 at 20:54):

Maybe but I don’t think so: it doesn’t use the scalar action on `f`

, but rather only on the module `M`

.

#### Oliver Nash (Mar 05 2021 at 20:54):

It seems totally ridiculous but I had to fuss about quite a bit to get a proof.

#### Adam Topaz (Mar 05 2021 at 20:54):

Oh I see.

#### Adam Topaz (Mar 05 2021 at 21:05):

Here's a sketch, but I can't find anything like `finsupp.foo`

either:

```
import linear_algebra
import data.finsupp.basic
variables {α R M N : Type*}
variables [semiring R] [add_comm_monoid M] [semimodule R M] [add_comm_monoid N] [semimodule R N]
variables {f : α →₀ M} {g : α → M → N}
lemma finsupp.foo (f1 f2 : α →₀ M) : (f1 + f2).sum g = f1.sum g + f2.sum g := sorry
-- TODO Convenient coercion to state using `g : α → M →[R] N` instead of the unbundled hypothesis ?
@[simp] lemma finsupp.smul_sum' (h : ∀ (t : R) a m, g a (t • m) = t • g a m) (t : R) :
(t • f).sum g = t • (f.sum g) :=
begin
apply finsupp.induction f,
simp,
intros a b f ha hb hh,
simp [finsupp.foo, hh],
congr,
rw [finsupp.sum_single_index, finsupp.sum_single_index, h],
sorry, sorry -- follows from linearity
end
```

#### Adam Topaz (Mar 05 2021 at 21:09):

oh, maybe this is it? docs#finsupp.sum_smul_index

#### Adam Topaz (Mar 05 2021 at 21:10):

No, not quite.

#### Adam Topaz (Mar 05 2021 at 21:11):

Ok, here it is golfed a bit:

```
import linear_algebra
import data.finsupp.basic
variables {α R M N : Type*}
variables [semiring R] [add_comm_monoid M] [semimodule R M] [add_comm_monoid N] [semimodule R N]
variables {f : α →₀ M} {g : α → M →ₗ[R] N}
-- TODO Convenient coercion to state using `g : α → M →[R] N` instead of the unbundled hypothesis ?
@[simp] lemma finsupp.smul_sum' (t : R) :
(t • f).sum (λ a, g a) = t • (f.sum (λ a, g a)) :=
begin
apply finsupp.induction f,
simp only [finsupp.sum_zero_index, smul_zero],
intros a b f ha hb hh,
simp [finsupp.sum_add_index, hh],
end
```

#### Adam Topaz (Mar 05 2021 at 21:11):

Note I changed `g`

#### Oliver Nash (Mar 05 2021 at 22:36):

Thanks, this is great :-) My horrid proof only assumed `g`

to be a family of `mul_action_hom`

s but in my application I have full linearity so I'll go with this.

#### Eric Wieser (Mar 05 2021 at 23:10):

There's definitely a one-line proof for this...

#### Eric Wieser (Mar 05 2021 at 23:15):

What's the statement for a general add_monoid_hom, not just `t \smul`

#### Eric Wieser (Mar 05 2021 at 23:31):

docs#add_monoid_hom.map_finsupp_sum applied to docs#smul_add_hom should be half of the puzzle I think

#### Oliver Nash (Mar 06 2021 at 18:04):

Eric Wieser said:

docs#add_monoid_hom.map_finsupp_sum applied to docs#smul_add_hom should be half of the puzzle I think

If I'm reading it right, docs#add_monoid_hom.map_finsupp_sum does not apply here. The `smul`

on the LHS of my `(t • f).sum g = t • (f.sum g)`

is a scalar action on `α →₀ M`

whereas the LHS of `map_finsupp_sum`

consumes `f.sum g`

which is an element of `N`

.

#### Oliver Nash (Mar 06 2021 at 18:05):

(Note also that I require a `semimodule`

structure for my statement to make sense.)

#### Oliver Nash (Mar 06 2021 at 18:05):

I wouldn't be surprised if there is a one-line proof and I would love if someone could find it (maybe GPTf :thinking:).

#### Oliver Nash (Mar 06 2021 at 18:07):

Eric Wieser said:

What's the statement for a general add_monoid_hom, not just

`t \smul`

This is a great point of course but if this result really is missing (as I now believe) then I think the corresponding general statement would use it, rather than the other way around. Anyway, I only have a few minutes so I'd better stop waffling and see if I can PR Adam's proof.

#### Oliver Nash (Mar 06 2021 at 18:53):

https://github.com/leanprover-community/mathlib/pull/6565

Last updated: May 16 2021 at 05:21 UTC