From 7de517b2eab45486d9c08ab835627c3bf6c754fb Mon Sep 17 00:00:00 2001
From: tb65536 <tb65536@uw.edu>
Date: Sat, 18 Dec 2021 14:23:56 +0000
Subject: [PATCH] feat(algebra/algebra/subalgebra): Elements of supremum
 (#10872)

Adds a few lemmas about elements of a supremum of subalgebras (essentially copied from the analogous lemmas in `group_theory/subgroup.basic`).
---
 src/algebra/algebra/subalgebra.lean | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/src/algebra/algebra/subalgebra.lean b/src/algebra/algebra/subalgebra.lean
index ee511a6fdace3..72cfe53999ded 100644
--- a/src/algebra/algebra/subalgebra.lean
+++ b/src/algebra/algebra/subalgebra.lean
@@ -530,6 +530,16 @@ set.mem_univ x
 
 @[simp] lemma top_to_subsemiring : (⊤ : subalgebra R A).to_subsemiring = ⊤ := rfl
 
+lemma mem_sup_left {S T : subalgebra R A} : ∀ {x : A}, x ∈ S → x ∈ S ⊔ T :=
+show S ≤ S ⊔ T, from le_sup_left
+
+lemma mem_sup_right {S T : subalgebra R A} : ∀ {x : A}, x ∈ T → x ∈ S ⊔ T :=
+show T ≤ S ⊔ T, from le_sup_right
+
+lemma mul_mem_sup {S T : subalgebra R A} {x y : A} (hx : x ∈ S) (hy : y ∈ T) :
+  x * y ∈ S ⊔ T :=
+(S ⊔ T).mul_mem (mem_sup_left hx) (mem_sup_right hy)
+
 @[simp, norm_cast]
 lemma coe_inf (S T : subalgebra R A) : (↑(S ⊓ T) : set A) = S ∩ T := rfl