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

theorem addLeftEmbedding.proof_1 {G : Type u_1} [AddLeftCancelSemigroup G] (g : G) : Function.Injective ((fun x x_1 => x + x_1) g)

def addLeftEmbedding {G : Type u_2} [AddLeftCancelSemigroup G] (g : G) : G ↪ G

The embedding of a left cancellative additive semigroup into itself by left translation by a fixed element.

@[simp]

theorem mulLeftEmbedding_apply {G : Type u_2} [LeftCancelSemigroup G] (g : G) (h : G) : ↑(mulLeftEmbedding g) h = g * h

@[simp]

theorem addLeftEmbedding_apply {G : Type u_2} [AddLeftCancelSemigroup G] (g : G) (h : G) : ↑(addLeftEmbedding g) h = g + h

def mulLeftEmbedding {G : Type u_2} [LeftCancelSemigroup G] (g : G) : G ↪ G

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

theorem addRightEmbedding.proof_1 {G : Type u_1} [AddRightCancelSemigroup G] (g : G) : Function.Injective fun x => x + g

def addRightEmbedding {G : Type u_2} [AddRightCancelSemigroup G] (g : G) : G ↪ G

The embedding of a right cancellative additive semigroup into itself by right translation by a fixed element.

@[simp]

theorem addRightEmbedding_apply {G : Type u_2} [AddRightCancelSemigroup G] (g : G) (h : G) : ↑(addRightEmbedding g) h = h + g

@[simp]

theorem mulRightEmbedding_apply {G : Type u_2} [RightCancelSemigroup G] (g : G) (h : G) : ↑(mulRightEmbedding g) h = h * g

def mulRightEmbedding {G : Type u_2} [RightCancelSemigroup G] (g : G) : G ↪ G

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

theorem addLeftEmbedding_eq_addRightEmbedding {G : Type u_2} [AddCancelCommMonoid G] (g : G) : addLeftEmbedding g = addRightEmbedding g

theorem mulLeftEmbedding_eq_mulRightEmbedding {G : Type u_2} [CancelCommMonoid G] (g : G) : mulLeftEmbedding g = mulRightEmbedding g