mem_span_of_mem_span

Stream: Is there code for X?

[Scott Morrison]

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]

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

[Scott Morrison]

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

suffices.

[Johan Commelin]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Johan Commelin]

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

[Ruben Van de Velde]

#1822 has a bit about iterating linear maps

[Scott Morrison]

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]

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