## 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,
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