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.

Equations

• mulLeftEmbedding g = { toFun := fun (h : G) => g * h, inj' := ⋯ }

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.

Equations

• addLeftEmbedding g = { toFun := fun (h : G) => g + h, inj' := ⋯ }

@[simp]

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

@[simp]

theorem mulLeftEmbedding_apply {G : Type u_1} [Mul G] [IsLeftCancelMul G] (g h : G) : (mulLeftEmbedding 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.

Equations

• mulRightEmbedding g = { toFun := fun (h : G) => h * g, inj' := ⋯ }

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.

Equations

• addRightEmbedding g = { toFun := fun (h : G) => h + g, inj' := ⋯ }

@[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} [CommSemigroup G] [IsCancelMul G] (g : G) : mulLeftEmbedding g = mulRightEmbedding g

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