# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: linear maps in the constructor for power_series

#### Moritz Firsching (Feb 21 2021 at 21:09):

I'm wondering if the following lemmas would be useful to have in mathlib, or are already in some form in mathlib, or if there is a reason why they (and similar lemmas basically translating the stuff from linear_map to power_series.mk) are not present there. I could need it in a theorem, but I can of course also make the proof of the theorem a little longer.

```
import tactic
import ring_theory.power_series.basic
open power_series
variables {σ R : Type*}
variables (R) [semiring R]
lemma mk_map_add (a b : ℕ → R): (mk (a) + mk (b)) = mk (λ p,(a p) + (b p)) :=
begin
ext,
simp only [coeff_mk, linear_map.map_add],
end
lemma mk_map_zero: mk(0:(ℕ → R)) = 0 :=
begin
ext,
simp only [coeff_mk, linear_map.map_zero, pi.zero_apply],
end
lemma mk_map_sum (f : ℕ → R) (S : finset ℕ):
mk (λ p, S.sum(f)) = S.sum(λ n, mk(λ p, f n)) :=
begin
ext,
simp only [coeff_mk, linear_map.map_sum],
end
```

#### Eric Wieser (Feb 21 2021 at 21:37):

A better strategy might be to show that `mk`

is an a `linear_map`

, and then the sum lemmas are free

#### Moritz Firsching (Feb 21 2021 at 21:40):

That makes sense!

#### Eric Wieser (Feb 21 2021 at 22:22):

Also, `λ p,(a p) + (b p)`

is just `a + b`

thanks to docs#pi.add_monoid

#### Fabian Kruse (Feb 22 2021 at 13:12):

I think this theorem should do it:

```
theorem pow_series_mk_is_lin_map (R : Type) [ring R]:
is_linear_map R (λ (f:ℕ→ R),mk(λ p, f p)) :=
begin
refine {map_add := _, map_smul := _},
repeat {intros, exact rfl},
end
```

Where should it be located? In module.linear_map?

#### Kevin Buzzard (Feb 22 2021 at 13:34):

I think that the preferred solution would be not to prove is_linear_map but to instead construct a term `mk'`

of type `linear_map`

Last updated: May 19 2021 at 02:10 UTC