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

ink

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

Equations

• (_ : Function.Injective ((fun x x_1 => x + x_1) g)) = (_ : Function.Injective ((fun x x_1 => x + x_1) g))

ink

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

• addLeftEmbedding g = { toFun := fun h => g + h, inj' := (_ : Function.Injective ((fun x x_1 => x + x_1) g)) }

ink

@[simp]

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

ink

@[simp]

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

ink

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

• mulLeftEmbedding g = { toFun := fun h => g * h, inj' := (_ : Function.Injective ((fun x x_1 => x * x_1) g)) }

ink

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

Equations

• (_ : Function.Injective fun x => x + g) = (_ : Function.Injective fun x => x + g)

ink

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

• addRightEmbedding g = { toFun := fun h => h + g, inj' := (_ : Function.Injective fun x => x + g) }

ink

@[simp]

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

ink

@[simp]

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

ink

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

• mulRightEmbedding g = { toFun := fun h => h * g, inj' := (_ : Function.Injective fun x => x * g) }

ink

theorem add_left_embedding_eq_add_right_embedding {G : Type u_1} [inst : AddCancelCommMonoid G] (g : G) : addLeftEmbedding g = addRightEmbedding g

ink

theorem mul_left_embedding_eq_mul_right_embedding {G : Type u_1} [inst : CancelCommMonoid G] (g : G) : mulLeftEmbedding g = mulRightEmbedding g