mathlib3 documentation

algebra.hom.embedding

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

def add_left_embedding {G : Type u_1} [add_left_cancel_semigroup G] (g : G) :
G G

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

Equations
def mul_left_embedding {G : Type u_1} [left_cancel_semigroup G] (g : G) :
G G

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

Equations
@[simp]
theorem add_left_embedding_apply {G : Type u_1} [add_left_cancel_semigroup G] (g h : G) :
@[simp]
theorem mul_left_embedding_apply {G : Type u_1} [left_cancel_semigroup G] (g h : G) :
@[simp]
def mul_right_embedding {G : Type u_1} [right_cancel_semigroup G] (g : G) :
G G

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

Equations
def add_right_embedding {G : Type u_1} [add_right_cancel_semigroup 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 mul_right_embedding_apply {G : Type u_1} [right_cancel_semigroup G] (g h : G) :