feat(ring_theory/adjoin/basic): lemmas relating adjoin and submodule.…

…span (#8031)

src/ring_theory/adjoin/basic.lean

@@ -97,6 +97,17 @@ begin
   exact submonoid.closure_le.2 subset_adjoin
 end
 
+lemma span_le_adjoin (s : set A) : span R s ≤ (adjoin R s).to_submodule :=
+span_le.mpr subset_adjoin
+
+lemma adjoin_to_submodule_le {s : set A} {t : submodule R A} :
+  (adjoin R s).to_submodule ≤ t ↔ ↑(submonoid.closure s) ⊆ (t : set A) :=
+by rw [adjoin_eq_span, span_le]
+
+lemma adjoin_eq_span_of_subset {s : set A} (hs : ↑(submonoid.closure s) ⊆ (span R s : set A)) :
+  (adjoin R s).to_submodule = span R s :=
+le_antisymm ((adjoin_to_submodule_le R).mpr hs) (span_le_adjoin R s)
+
 lemma adjoin_image (f : A →ₐ[R] B) (s : set A) :
   adjoin R (f '' s) = (adjoin R s).map f :=
 le_antisymm (adjoin_le $ set.image_subset _ subset_adjoin) $