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 : AddLeftCancelSemigroup G] (g : G) :
Function.Injective ((fun x x_1 => x + x_1) g)
Equations
def addLeftEmbedding {G : Type u_1} [inst : AddLeftCancelSemigroup G] (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 : LeftCancelSemigroup G] (g : G) (h : G) :
↑(mulLeftEmbedding g) h = g * h
@[simp]
theorem addLeftEmbedding_apply {G : Type u_1} [inst : AddLeftCancelSemigroup G] (g : G) (h : G) :
↑(addLeftEmbedding g) h = g + h
def mulLeftEmbedding {G : Type u_1} [inst : LeftCancelSemigroup G] (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 : AddRightCancelSemigroup G] (g : G) :
Function.Injective fun x => x + g
Equations
def addRightEmbedding {G : Type u_1} [inst : AddRightCancelSemigroup G] (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 : AddRightCancelSemigroup G] (g : G) (h : G) :
↑(addRightEmbedding g) h = h + g
@[simp]
theorem mulRightEmbedding_apply {G : Type u_1} [inst : RightCancelSemigroup G] (g : G) (h : G) :
↑(mulRightEmbedding g) h = h * g
def mulRightEmbedding {G : Type u_1} [inst : RightCancelSemigroup G] (g : G) :
G G

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

Equations