feat(ring_theory/ideal/basic): add ideal.span_pair lemmas (#18036)

src/ring_theory/ideal/basic.lean

@@ -260,10 +260,26 @@ begin
   exact hmax M (lt_of_lt_of_le hPJ hM2) hM1,
 end
 
+lemma span_pair_comm {x y : α} : (span {x, y} : ideal α) = span {y, x} :=
+by simp only [span_insert, sup_comm]
+
 theorem mem_span_pair {x y z : α} :
   z ∈ span ({x, y} : set α) ↔ ∃ a b, a * x + b * y = z :=
 by simp [mem_span_insert, mem_span_singleton', @eq_comm _ _ z]
 
+@[simp] lemma span_pair_add_mul_left {R : Type u} [comm_ring R] {x y : R} (z : R) :
+  (span {x + y * z, y} : ideal R) = span {x, y} :=
+begin
+  ext,
+  rw [mem_span_pair, mem_span_pair],
+  exact ⟨λ ⟨a, b, h⟩, ⟨a, b + a * z, by { rw [← h], ring1 }⟩,
+         λ ⟨a, b, h⟩, ⟨a, b - a * z, by { rw [← h], ring1 }⟩⟩
+end
+
+@[simp] lemma span_pair_add_mul_right {R : Type u} [comm_ring R] {x y : R} (z : R) :
+  (span {x, y + x * z} : ideal R) = span {x, y} :=
+by rw [span_pair_comm, span_pair_add_mul_left, span_pair_comm]
+
 theorem is_maximal.exists_inv {I : ideal α}
   (hI : I.is_maximal) {x} (hx : x ∉ I) : ∃ y, ∃ i ∈ I, y * x + i = 1 :=
 begin