## Stream: new members

### Topic: smul_mem_span

#### Alexander Bentkamp (May 17 2019 at 14:03):

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 (May 17 2019 at 14:12):

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

#### Alexander Bentkamp (May 17 2019 at 14:46):

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

Last updated: May 08 2021 at 10:12 UTC