Zulip Chat Archive

Stream: Is there code for X?

Topic: linear maps in the constructor for power_series


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Moritz Firsching (Feb 21 2021 at 21:40):

That makes sense!

view this post on Zulip Eric Wieser (Feb 21 2021 at 22:22):

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

view this post on Zulip 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?

view this post on Zulip 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