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.

source
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
source
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
source
@[simp]
theorem add_left_embedding_apply {G : Type u_1} [add_left_cancel_semigroup G] (g h : G) :
⇑(add_left_embedding g) h = g + h
source
@[simp]
theorem mul_left_embedding_apply {G : Type u_1} [left_cancel_semigroup G] (g h : G) :
⇑(mul_left_embedding g) h = g * h
source
@[simp]
theorem add_right_embedding_apply {G : Type u_1} [add_right_cancel_semigroup G] (g h : G) :
⇑(add_right_embedding g) h = h + g
source
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
source
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
source
@[simp]
theorem mul_right_embedding_apply {G : Type u_1} [right_cancel_semigroup G] (g h : G) :
⇑(mul_right_embedding g) h = h * g
source
theorem mul_left_embedding_eq_mul_right_embedding {G : Type u_1} [cancel_comm_monoid G] (g : G) :
mul_left_embedding g = mul_right_embedding g
source
theorem add_left_embedding_eq_add_right_embedding {G : Type u_1} [add_cancel_comm_monoid G] (g : G) :
add_left_embedding g = add_right_embedding g