Zulip Chat Archive

Stream: new members

Topic: smul_mem_span


view this post on Zulip 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 :=

view this post on Zulip 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.

view this post on Zulip 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