feat(linear_algebra/basic, ring_theory/ideal/basic): add span_insert (#…

…9941)

src/linear_algebra/basic.lean

@@ -1047,6 +1047,9 @@ begin
   simp only [eq_comm, add_comm, exists_and_distrib_left]
 end
 
+lemma span_insert (x) (s : set M) : span R (insert x s) = span R ({x} : set M) ⊔ span R s :=
+by rw [insert_eq, span_union]
+
 lemma span_insert_eq_span (h : x ∈ span R s) : span R (insert x s) = span R s :=
 span_eq_of_le _ (set.insert_subset.mpr ⟨h, subset_span⟩) (span_mono $ subset_insert _ _)
 

src/ring_theory/ideal/basic.lean

@@ -100,6 +100,9 @@ lemma mem_span_insert {s : set α} {x y} :
 lemma mem_span_singleton' {x y : α} :
   x ∈ span ({y} : set α) ↔ ∃ a, a * y = x := submodule.mem_span_singleton
 
+lemma span_insert (x) (s : set α) : span (insert x s) = span ({x} : set α) ⊔ span s :=
+submodule.span_insert x s
+
 lemma span_eq_bot {s : set α} : span s = ⊥ ↔ ∀ x ∈ s, (x:α) = 0 := submodule.span_eq_bot
 
 @[simp] lemma span_singleton_eq_bot {x} : span ({x} : set α) = ⊥ ↔ x = 0 :=