feat(combinatorics/additive/salem_spencer): Salem-Spencer sets and Ro…

…th numbers (#10509) This defines Salem-Spencer sets and Roth numbers in (additive) monoids. Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
leanprover-community · Dec 13, 2021 · 108eb0b · 108eb0b
1 parent e174736
commit 108eb0b
Show file tree

Hide file tree

Showing 3 changed files with 428 additions and 0 deletions.
diff --git a/src/algebra/regular/basic.lean b/src/algebra/regular/basic.lean
@@ -268,6 +268,11 @@ by right multiplication by a fixed element.
 def mul_right_embedding {G : Type*} [right_cancel_semigroup G] (g : G) : G ↪ G :=
 { to_fun := λ h, h * g, inj' := mul_left_injective g }
 
+@[to_additive]
+lemma mul_left_embedding_eq_mul_right_embedding {G : Type*} [cancel_comm_monoid G] (g : G) :
+  mul_left_embedding g = mul_right_embedding g :=
+by { ext, exact mul_comm _ _ }
+
 /--  Elements of a left cancel semigroup are left regular. -/
 lemma is_left_regular_of_left_cancel_semigroup [left_cancel_semigroup R] (g : R) :
   is_left_regular g :=