smul_mem_span

Stream: new members

[Alexander Bentkamp]

Does this lemma really not exist yet?

lemma smul_mem_span {α β : Type} [ring α] [add_comm_group β] [module α β]
  (a : α) (x : β) (s : set β) (h : x ∈ span α s) :
  a • x ∈ span α s :=

[Sebastien Gouezel]

This has nothing to do with spans, it is a fact on submodules. Try submodule.smul _ _ h.

[Alexander Bentkamp]

Oh right. I found this out once before and forgot again :-)