Zulip Chat Archive

Stream: Is there code for X?

Topic: Member of a set is a member of its span


view this post on Zulip Ashvni Narayanan (Jan 05 2021 at 08:19):

I have a feeling the following lemma should exist somewhere :

import ring_theory.fractional_ideal

open_locale classical

variables (B : Type*) [semiring B]
variables (M : Type*) [add_comm_monoid M] [semimodule B M]

open submodule

lemma mem_span_set (x : M) (S : set M) (hx : x  S) : x  span B S :=
begin
  suffices f : S  span B S,
  apply iff.rfl.1 f hx,
  apply submodule.subset_span,
end

Any help is appreciated, thank you!

view this post on Zulip Kenny Lau (Jan 05 2021 at 08:20):

This is just submodule.subset_span

view this post on Zulip Kenny Lau (Jan 05 2021 at 08:20):

lemma mem_span_set (x : M) (S : set M) (hx : x  S) : x  span B S :=
submodule.subset_span hx

view this post on Zulip Patrick Massot (Jan 05 2021 at 08:21):

Ashvni, the proof of your suffices is iff.rfl, so you don't need it.

view this post on Zulip Ashvni Narayanan (Jan 05 2021 at 08:22):

I see, thank you!

view this post on Zulip Kevin Buzzard (Jan 05 2021 at 08:22):

The point is that ABA\subseteq B is definitionally equal to x,xA    xB\forall x, x\in A \implies x\in B

view this post on Zulip Ashvni Narayanan (Jan 05 2021 at 08:26):

I get it now, thank you!


Last updated: May 17 2021 at 16:26 UTC