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
• = { toFun := fun (h : G) => g + h, inj' := }
Instances For
@[simp]
theorem addLeftEmbedding_apply {G : Type u_1} [Add G] [] (g : G) (h : G) :
h = g + h
@[simp]
theorem mulLeftEmbedding_apply {G : Type u_1} [Mul 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
• = { toFun := fun (h : G) => g * h, inj' := }
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
• = { toFun := fun (h : G) => h + g, inj' := }
Instances For
@[simp]
theorem addRightEmbedding_apply {G : Type u_1} [Add G] [] (g : G) (h : G) :
h = h + g
@[simp]
theorem mulRightEmbedding_apply {G : Type u_1} [Mul 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
• = { toFun := fun (h : G) => h * g, inj' := }
Instances For
theorem addLeftEmbedding_eq_addRightEmbedding {G : Type u_1} [] [] (g : G) :
theorem mulLeftEmbedding_eq_mulRightEmbedding {G : Type u_1} [] [] (g : G) :