Documentation

Mathlib.Algebra.Group.Embedding

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

source
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.

Instances For
    source
    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.

    Instances For
      source
      @[simp]
      theorem mulLeftEmbedding_apply {G : Type u_1} [Mul G] [IsLeftCancelMul G] (g h : G) :
      (mulLeftEmbedding g) h = g * h
      source
      @[simp]
      theorem addLeftEmbedding_apply {G : Type u_1} [Add G] [IsLeftCancelAdd G] (g h : G) :
      (addLeftEmbedding g) h = g + h
      source
      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.

      Instances For
        source
        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.

        Instances For
          source
          @[simp]
          theorem mulRightEmbedding_apply {G : Type u_1} [Mul G] [IsRightCancelMul G] (g h : G) :
          (mulRightEmbedding g) h = h * g
          source
          @[simp]
          theorem addRightEmbedding_apply {G : Type u_1} [Add G] [IsRightCancelAdd G] (g h : G) :
          (addRightEmbedding g) h = h + g
          source
          theorem mulLeftEmbedding_eq_mulRightEmbedding {G : Type u_1} [CommMagma G] [IsCancelMul G] (g : G) :
          mulLeftEmbedding g = mulRightEmbedding g
          source
          theorem addLeftEmbedding_eq_addRightEmbedding {G : Type u_1} [AddCommMagma G] [IsCancelAdd G] (g : G) :
          addLeftEmbedding g = addRightEmbedding g