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] [IsLeftCancelAdd 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 addLeftEmbedding_apply {G : Type u_1} [Add G] [IsLeftCancelAdd G] (g : G) (h : G) :
    (addLeftEmbedding g) h = g + h
    @[simp]
    theorem mulLeftEmbedding_apply {G : Type u_1} [Mul G] [IsLeftCancelMul G] (g : G) (h : G) :
    (mulLeftEmbedding g) h = g * h
    def mulLeftEmbedding {G : Type u_1} [Mul G] [IsLeftCancelMul 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] [IsRightCancelAdd 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 addRightEmbedding_apply {G : Type u_1} [Add G] [IsRightCancelAdd G] (g : G) (h : G) :
        @[simp]
        theorem mulRightEmbedding_apply {G : Type u_1} [Mul G] [IsRightCancelMul G] (g : G) (h : G) :
        def mulRightEmbedding {G : Type u_1} [Mul G] [IsRightCancelMul G] (g : G) :
        G G

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

        Equations
        Instances For