# Documentation

Mathlib.Algebra.Group.Embedding

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

def addLeftEmbedding {G : Type u_1} [Add G] [] (g : G) :
G G

If left-addition by any element is cancellative, left-addition by g is an embedding.

Equations
Instances For
@[simp]
theorem mulLeftEmbedding_apply {G : Type u_1} [Mul G] [] (g : G) (h : G) :
() h = g * h
@[simp]
theorem addLeftEmbedding_apply {G : Type u_1} [Add G] [] (g : G) (h : G) :
() h = g + h
def mulLeftEmbedding {G : Type u_1} [Mul G] [] (g : G) :
G G

If left-multiplication by any element is cancellative, left-multiplication by g is an embedding.

Equations
Instances For
def addRightEmbedding {G : Type u_1} [Add G] [] (g : G) :
G G

If right-addition by any element is cancellative, right-addition by g is an embedding.

Equations
Instances For
@[simp]
theorem mulRightEmbedding_apply {G : Type u_1} [Mul G] [] (g : G) (h : G) :
h = h * g
@[simp]
theorem addRightEmbedding_apply {G : Type u_1} [Add G] [] (g : G) (h : G) :
h = h + g
def mulRightEmbedding {G : Type u_1} [Mul G] [] (g : G) :
G G

If right-multiplication by any element is cancellative, right-multiplication by g is an embedding.

Equations
Instances For
theorem addLeftEmbedding_eq_addRightEmbedding {G : Type u_1} [] [] (g : G) :
theorem mulLeftEmbedding_eq_mulRightEmbedding {G : Type u_1} [] [] (g : G) :