## Stream: Is there code for X?

### Topic: mem_span_of_mem_span

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


#### Scott Morrison (Feb 23 2021 at 09:41):

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

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

#### Johan Commelin (Feb 23 2021 at 09:42):

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

#### Scott Morrison (Feb 23 2021 at 09:48):

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

#### Scott Morrison (Feb 23 2021 at 09:48):

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

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

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

#### Ruben Van de Velde (Feb 23 2021 at 10:24):

#1822 has a bit about iterating linear maps

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

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