# Documentation

Mathlib.Algebra.Hom.Embedding

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

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

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

Instances For
@[simp]
theorem mulLeftEmbedding_apply {G : Type u_2} (g : G) (h : G) :
↑() h = g * h
@[simp]
theorem addLeftEmbedding_apply {G : Type u_2} (g : G) (h : G) :
↑() h = g + h
def mulLeftEmbedding {G : Type u_2} (g : G) :
G G

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

Instances For
theorem addRightEmbedding.proof_1 {G : Type u_1} (g : G) :
Function.Injective fun x => x + g
def addRightEmbedding {G : Type u_2} (g : G) :
G G

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

Instances For
@[simp]
theorem addRightEmbedding_apply {G : Type u_2} (g : G) (h : G) :
↑() h = h + g
@[simp]
theorem mulRightEmbedding_apply {G : Type u_2} (g : G) (h : G) :
↑() h = h * g
def mulRightEmbedding {G : Type u_2} (g : G) :
G G

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

Instances For
theorem mulLeftEmbedding_eq_mulRightEmbedding {G : Type u_2} [] (g : G) :