# Documentation

Mathlib.Algebra.Hom.Embedding

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

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

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

Equations
@[simp]
theorem mulLeftEmbedding_apply {G : Type u_1} [inst : ] (g : G) (h : G) :
↑() h = g * h
@[simp]
theorem addLeftEmbedding_apply {G : Type u_1} [inst : ] (g : G) (h : G) :
↑() h = g + h
def mulLeftEmbedding {G : Type u_1} [inst : ] (g : G) :
G G

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

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

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

Equations
@[simp]
theorem addRightEmbedding_apply {G : Type u_1} [inst : ] (g : G) (h : G) :
↑() h = h + g
@[simp]
theorem mulRightEmbedding_apply {G : Type u_1} [inst : ] (g : G) (h : G) :
↑() h = h * g
def mulRightEmbedding {G : Type u_1} [inst : ] (g : G) :
G G

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

Equations
theorem add_left_embedding_eq_add_right_embedding {G : Type u_1} [inst : ] (g : G) :
theorem mul_left_embedding_eq_mul_right_embedding {G : Type u_1} [inst : ] (g : G) :