linear maps in the constructor for power_series

Stream: Is there code for X?

[Moritz Firsching]

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]

A better strategy might be to show that mk is an a linear_map, and then the sum lemmas are free

[Moritz Firsching]

That makes sense!

[Eric Wieser]

Also, λ p,(a p) + (b p) is just a + b thanks to docs#pi.add_monoid

[Fabian Kruse]

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]

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