Zulip Chat Archive

Stream: Is there code for X?

Topic: mem_span_of_mem_span


view this post on Zulip Scott Morrison (Feb 23 2021 at 09:41):

lemma apply_mem_span_of_mem_span {R : Type*} [semiring R]
   {M : Type*} [add_comm_monoid M] [semimodule R M]
   {N : Type*} [add_comm_monoid N] [semimodule R N]
   (f : M →ₗ[R] N) {x : M} {s : set M} (h : x  submodule.span R s) :
   f x  submodule.span R (f '' s) :=
by is_there_code_for_X

view this post on Zulip Scott Morrison (Feb 23 2021 at 09:41):

is hopefully in the library somewhere already, and I'm just not finding it.

view this post on Zulip Scott Morrison (Feb 23 2021 at 09:41):

begin
  simp only [submodule.mem_span, submodule.mem_map, submodule.span_image] at h ,
  exact x, h, rfl⟩⟩,
end

suffices.

view this post on Zulip Johan Commelin (Feb 23 2021 at 09:42):

I wouldn't be surprised it is missing...

view this post on Zulip Scott Morrison (Feb 23 2021 at 09:48):

I'm remembering why I avoid doing linear algebra in lean...

view this post on Zulip Scott Morrison (Feb 23 2021 at 09:48):

Relatedly, do we have iterates of linear maps, as a bundled linear map?

view this post on Zulip Scott Morrison (Feb 23 2021 at 09:49):

I found src/algebra/iterate_hom.lean, but this is just the lemmas about nat.iterate applied to a *_hom.

view this post on Zulip Johan Commelin (Feb 23 2021 at 09:54):

I'm not aware of such iterates. @Anne Baanen do you know if this is in mathlib?

view this post on Zulip Ruben Van de Velde (Feb 23 2021 at 10:24):

#1822 has a bit about iterating linear maps

view this post on Zulip Scott Morrison (Feb 23 2021 at 10:48):

Thanks. It's a pity the easy bits there about iterate didn't make it into mathlib when the rest of the PR stalled.

view this post on Zulip Ruben Van de Velde (Feb 23 2021 at 13:07):

Scott Morrison said:

Thanks. It's a pity the easy bits there about iterate didn't make it into mathlib when the rest of the PR stalled.

That's fixable - #6377


Last updated: May 17 2021 at 16:26 UTC