The embedding of a cancellative semigroup into itself by multiplication by a fixed element.

def mulLeftEmbedding {G : Type u_1} [Mul G] [IsLeftCancelMul G] (g : G) : G ↪ G

If left-multiplication by any element is cancellative, left-multiplication by g is an embedding.

def addLeftEmbedding {G : Type u_1} [Add G] [IsLeftCancelAdd G] (g : G) : G ↪ G

If left-addition by any element is cancellative, left-addition by g is an embedding.

@[simp]

theorem mulLeftEmbedding_apply {G : Type u_1} [Mul G] [IsLeftCancelMul G] (g h : G) : (mulLeftEmbedding g) h = g * h

@[simp]

theorem addLeftEmbedding_apply {G : Type u_1} [Add G] [IsLeftCancelAdd G] (g h : G) : (addLeftEmbedding g) h = g + h

def mulRightEmbedding {G : Type u_1} [Mul G] [IsRightCancelMul G] (g : G) : G ↪ G

If right-multiplication by any element is cancellative, right-multiplication by g is an embedding.

def addRightEmbedding {G : Type u_1} [Add G] [IsRightCancelAdd G] (g : G) : G ↪ G

If right-addition by any element is cancellative, right-addition by g is an embedding.

@[simp]

theorem mulRightEmbedding_apply {G : Type u_1} [Mul G] [IsRightCancelMul G] (g h : G) : (mulRightEmbedding g) h = h * g

@[simp]

theorem addRightEmbedding_apply {G : Type u_1} [Add G] [IsRightCancelAdd G] (g h : G) : (addRightEmbedding g) h = h + g

theorem mulLeftEmbedding_eq_mulRightEmbedding {G : Type u_1} [CommMagma G] [IsCancelMul G] (g : G) : mulLeftEmbedding g = mulRightEmbedding g

theorem addLeftEmbedding_eq_addRightEmbedding {G : Type u_1} [AddCommMagma G] [IsCancelAdd G] (g : G) : addLeftEmbedding g = addRightEmbedding g