Documentation

Mathlib.Algebra.Free

Free constructions #

Main definitions #

inductive FreeAddMagma (α : Type u) :

Free nonabelian additive magma over a given alphabet.

Instances For
    instance instDecidableEqFreeAddMagma :
    {α : Type u_1} → [inst : DecidableEq α] → DecidableEq (FreeAddMagma α)
    Equations
    • instDecidableEqFreeAddMagma = decEqFreeAddMagma✝
    inductive FreeMagma (α : Type u) :

    Free magma over a given alphabet.

    Instances For
      instance instDecidableEqFreeMagma :
      {α : Type u_1} → [inst : DecidableEq α] → DecidableEq (FreeMagma α)
      Equations
      • instDecidableEqFreeMagma = decEqFreeMagma✝
      Equations
      Equations
      instance FreeAddMagma.instAdd {α : Type u} :
      Equations
      • FreeAddMagma.instAdd = { add := FreeAddMagma.add }
      instance FreeMagma.instMul {α : Type u} :
      Equations
      • FreeMagma.instMul = { mul := FreeMagma.mul }
      @[simp]
      theorem FreeAddMagma.add_eq {α : Type u} (x : FreeAddMagma α) (y : FreeAddMagma α) :
      x.add y = x + y
      @[simp]
      theorem FreeMagma.mul_eq {α : Type u} (x : FreeMagma α) (y : FreeMagma α) :
      x.mul y = x * y
      def FreeAddMagma.recOnAdd {α : Type u} {C : FreeAddMagma αSort l} (x : FreeAddMagma α) (ih1 : (x : α) → C (FreeAddMagma.of x)) (ih2 : (x y : FreeAddMagma α) → C xC yC (x + y)) :
      C x

      Recursor for FreeAddMagma using x + y instead of FreeAddMagma.add x y.

      Equations
      Instances For
        def FreeMagma.recOnMul {α : Type u} {C : FreeMagma αSort l} (x : FreeMagma α) (ih1 : (x : α) → C (FreeMagma.of x)) (ih2 : (x y : FreeMagma α) → C xC yC (x * y)) :
        C x

        Recursor for FreeMagma using x * y instead of FreeMagma.mul x y.

        Equations
        Instances For
          theorem FreeAddMagma.hom_ext {α : Type u} {β : Type v} [Add β] {f : AddHom (FreeAddMagma α) β} {g : AddHom (FreeAddMagma α) β} (h : f FreeAddMagma.of = g FreeAddMagma.of) :
          f = g
          theorem FreeMagma.hom_ext {α : Type u} {β : Type v} [Mul β] {f : FreeMagma α →ₙ* β} {g : FreeMagma α →ₙ* β} (h : f FreeMagma.of = g FreeMagma.of) :
          f = g
          def FreeMagma.liftAux {α : Type u} {β : Type v} [Mul β] (f : αβ) :
          FreeMagma αβ

          Lifts a function α → β to a magma homomorphism FreeMagma α → β given a magma β.

          Equations
          Instances For
            def FreeAddMagma.liftAux {α : Type u} {β : Type v} [Add β] (f : αβ) :
            FreeAddMagma αβ

            Lifts a function α → β to an additive magma homomorphism FreeAddMagma α → β given an additive magma β.

            Equations
            Instances For
              theorem FreeAddMagma.lift.proof_2 {α : Type u_1} {β : Type u_2} [Add β] (f : αβ) :
              (fun (F : AddHom (FreeAddMagma α) β) => F FreeAddMagma.of) ((fun (f : αβ) => { toFun := FreeAddMagma.liftAux f, map_add' := }) f) = (fun (F : AddHom (FreeAddMagma α) β) => F FreeAddMagma.of) ((fun (f : αβ) => { toFun := FreeAddMagma.liftAux f, map_add' := }) f)
              theorem FreeAddMagma.lift.proof_1 {α : Type u_1} {β : Type u_2} [Add β] (f : αβ) (x : FreeAddMagma α) (y : FreeAddMagma α) :
              theorem FreeAddMagma.lift.proof_3 {α : Type u_1} {β : Type u_2} [Add β] (F : AddHom (FreeAddMagma α) β) :
              (fun (f : αβ) => { toFun := FreeAddMagma.liftAux f, map_add' := }) ((fun (F : AddHom (FreeAddMagma α) β) => F FreeAddMagma.of) F) = F
              def FreeAddMagma.lift {α : Type u} {β : Type v} [Add β] :
              (αβ) AddHom (FreeAddMagma α) β

              The universal property of the free additive magma expressing its adjointness.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[simp]
                theorem FreeMagma.lift_symm_apply {α : Type u} {β : Type v} [Mul β] (F : FreeMagma α →ₙ* β) :
                ∀ (a : α), FreeMagma.lift.symm F a = (F FreeMagma.of) a
                @[simp]
                theorem FreeAddMagma.lift_symm_apply {α : Type u} {β : Type v} [Add β] (F : AddHom (FreeAddMagma α) β) :
                ∀ (a : α), FreeAddMagma.lift.symm F a = (F FreeAddMagma.of) a
                def FreeMagma.lift {α : Type u} {β : Type v} [Mul β] :
                (αβ) (FreeMagma α →ₙ* β)

                The universal property of the free magma expressing its adjointness.

                Equations
                • FreeMagma.lift = { toFun := fun (f : αβ) => { toFun := FreeMagma.liftAux f, map_mul' := }, invFun := fun (F : FreeMagma α →ₙ* β) => F FreeMagma.of, left_inv := , right_inv := }
                Instances For
                  @[simp]
                  theorem FreeAddMagma.lift_of {α : Type u} {β : Type v} [Add β] (f : αβ) (x : α) :
                  (FreeAddMagma.lift f) (FreeAddMagma.of x) = f x
                  @[simp]
                  theorem FreeMagma.lift_of {α : Type u} {β : Type v} [Mul β] (f : αβ) (x : α) :
                  (FreeMagma.lift f) (FreeMagma.of x) = f x
                  @[simp]
                  theorem FreeAddMagma.lift_comp_of {α : Type u} {β : Type v} [Add β] (f : αβ) :
                  (FreeAddMagma.lift f) FreeAddMagma.of = f
                  @[simp]
                  theorem FreeMagma.lift_comp_of {α : Type u} {β : Type v} [Mul β] (f : αβ) :
                  (FreeMagma.lift f) FreeMagma.of = f
                  @[simp]
                  theorem FreeAddMagma.lift_comp_of' {α : Type u} {β : Type v} [Add β] (f : AddHom (FreeAddMagma α) β) :
                  FreeAddMagma.lift (f FreeAddMagma.of) = f
                  @[simp]
                  theorem FreeMagma.lift_comp_of' {α : Type u} {β : Type v} [Mul β] (f : FreeMagma α →ₙ* β) :
                  FreeMagma.lift (f FreeMagma.of) = f
                  def FreeAddMagma.map {α : Type u} {β : Type v} (f : αβ) :

                  The unique additive magma homomorphism FreeAddMagma α → FreeAddMagma β that sends each of x to of (f x).

                  Equations
                  Instances For
                    def FreeMagma.map {α : Type u} {β : Type v} (f : αβ) :

                    The unique magma homomorphism FreeMagma α →ₙ* FreeMagma β that sends each of x to of (f x).

                    Equations
                    Instances For
                      @[simp]
                      theorem FreeAddMagma.map_of {α : Type u} {β : Type v} (f : αβ) (x : α) :
                      @[simp]
                      theorem FreeMagma.map_of {α : Type u} {β : Type v} (f : αβ) (x : α) :
                      def FreeAddMagma.recOnPure {α : Type u} {C : FreeAddMagma αSort l} (x : FreeAddMagma α) (ih1 : (x : α) → C (pure x)) (ih2 : (x y : FreeAddMagma α) → C xC yC (x + y)) :
                      C x

                      Recursor on FreeAddMagma using pure instead of of.

                      Equations
                      • x.recOnPure ih1 ih2 = x.recOnAdd ih1 ih2
                      Instances For
                        def FreeMagma.recOnPure {α : Type u} {C : FreeMagma αSort l} (x : FreeMagma α) (ih1 : (x : α) → C (pure x)) (ih2 : (x y : FreeMagma α) → C xC yC (x * y)) :
                        C x

                        Recursor on FreeMagma using pure instead of of.

                        Equations
                        • x.recOnPure ih1 ih2 = x.recOnMul ih1 ih2
                        Instances For
                          @[simp]
                          theorem FreeAddMagma.map_pure {α : Type u} {β : Type u} (f : αβ) (x : α) :
                          f <$> pure x = pure (f x)
                          @[simp]
                          theorem FreeMagma.map_pure {α : Type u} {β : Type u} (f : αβ) (x : α) :
                          f <$> pure x = pure (f x)
                          @[simp]
                          theorem FreeAddMagma.map_add' {α : Type u} {β : Type u} (f : αβ) (x : FreeAddMagma α) (y : FreeAddMagma α) :
                          f <$> (x + y) = f <$> x + f <$> y
                          @[simp]
                          theorem FreeMagma.map_mul' {α : Type u} {β : Type u} (f : αβ) (x : FreeMagma α) (y : FreeMagma α) :
                          f <$> (x * y) = f <$> x * f <$> y
                          @[simp]
                          theorem FreeAddMagma.pure_bind {α : Type u} {β : Type u} (f : αFreeAddMagma β) (x : α) :
                          pure x >>= f = f x
                          @[simp]
                          theorem FreeMagma.pure_bind {α : Type u} {β : Type u} (f : αFreeMagma β) (x : α) :
                          pure x >>= f = f x
                          @[simp]
                          theorem FreeAddMagma.add_bind {α : Type u} {β : Type u} (f : αFreeAddMagma β) (x : FreeAddMagma α) (y : FreeAddMagma α) :
                          x + y >>= f = (x >>= f) + (y >>= f)
                          @[simp]
                          theorem FreeMagma.mul_bind {α : Type u} {β : Type u} (f : αFreeMagma β) (x : FreeMagma α) (y : FreeMagma α) :
                          x * y >>= f = (x >>= f) * (y >>= f)
                          @[simp]
                          theorem FreeAddMagma.pure_seq {α : Type u} {β : Type u} {f : αβ} {x : FreeAddMagma α} :
                          (Seq.seq (pure f) fun (x_1 : Unit) => x) = f <$> x
                          @[simp]
                          theorem FreeMagma.pure_seq {α : Type u} {β : Type u} {f : αβ} {x : FreeMagma α} :
                          (Seq.seq (pure f) fun (x_1 : Unit) => x) = f <$> x
                          @[simp]
                          theorem FreeAddMagma.add_seq {α : Type u} {β : Type u} {f : FreeAddMagma (αβ)} {g : FreeAddMagma (αβ)} {x : FreeAddMagma α} :
                          (Seq.seq (f + g) fun (x_1 : Unit) => x) = (Seq.seq f fun (x_1 : Unit) => x) + Seq.seq g fun (x_1 : Unit) => x
                          @[simp]
                          theorem FreeMagma.mul_seq {α : Type u} {β : Type u} {f : FreeMagma (αβ)} {g : FreeMagma (αβ)} {x : FreeMagma α} :
                          (Seq.seq (f * g) fun (x_1 : Unit) => x) = (Seq.seq f fun (x_1 : Unit) => x) * Seq.seq g fun (x_1 : Unit) => x
                          def FreeMagma.traverse {m : Type u → Type u} [Applicative m] {α : Type u} {β : Type u} (F : αm β) :
                          FreeMagma αm (FreeMagma β)

                          FreeMagma is traversable.

                          Equations
                          Instances For
                            def FreeAddMagma.traverse {m : Type u → Type u} [Applicative m] {α : Type u} {β : Type u} (F : αm β) :

                            FreeAddMagma is traversable.

                            Equations
                            Instances For
                              @[simp]
                              theorem FreeAddMagma.traverse_pure {α : Type u} {β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) (x : α) :
                              traverse F (pure x) = pure <$> F x
                              @[simp]
                              theorem FreeMagma.traverse_pure {α : Type u} {β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) (x : α) :
                              traverse F (pure x) = pure <$> F x
                              @[simp]
                              theorem FreeAddMagma.traverse_pure' {α : Type u} {β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) :
                              traverse F pure = fun (x : α) => pure <$> F x
                              @[simp]
                              theorem FreeMagma.traverse_pure' {α : Type u} {β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) :
                              traverse F pure = fun (x : α) => pure <$> F x
                              @[simp]
                              theorem FreeAddMagma.traverse_add {α : Type u} {β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) (x : FreeAddMagma α) (y : FreeAddMagma α) :
                              traverse F (x + y) = Seq.seq ((fun (x x_1 : FreeAddMagma β) => x + x_1) <$> traverse F x) fun (x : Unit) => traverse F y
                              @[simp]
                              theorem FreeMagma.traverse_mul {α : Type u} {β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) (x : FreeMagma α) (y : FreeMagma α) :
                              traverse F (x * y) = Seq.seq ((fun (x x_1 : FreeMagma β) => x * x_1) <$> traverse F x) fun (x : Unit) => traverse F y
                              @[simp]
                              theorem FreeAddMagma.traverse_add' {α : Type u} {β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) :
                              Function.comp (traverse F) HAdd.hAdd = fun (x y : FreeAddMagma α) => Seq.seq ((fun (x x_1 : FreeAddMagma β) => x + x_1) <$> traverse F x) fun (x : Unit) => traverse F y
                              @[simp]
                              theorem FreeMagma.traverse_mul' {α : Type u} {β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) :
                              Function.comp (traverse F) HMul.hMul = fun (x y : FreeMagma α) => Seq.seq ((fun (x x_1 : FreeMagma β) => x * x_1) <$> traverse F x) fun (x : Unit) => traverse F y
                              @[simp]
                              theorem FreeAddMagma.traverse_eq {α : Type u} {β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) (x : FreeAddMagma α) :
                              @[simp]
                              theorem FreeMagma.traverse_eq {α : Type u} {β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) (x : FreeMagma α) :
                              @[simp]
                              theorem FreeAddMagma.add_map_seq {α : Type u} (x : FreeAddMagma α) (y : FreeAddMagma α) :
                              (Seq.seq ((fun (x x_1 : FreeAddMagma α) => x + x_1) <$> x) fun (x : Unit) => y) = x + y
                              @[simp]
                              theorem FreeMagma.mul_map_seq {α : Type u} (x : FreeMagma α) (y : FreeMagma α) :
                              (Seq.seq ((fun (x x_1 : FreeMagma α) => x * x_1) <$> x) fun (x : Unit) => y) = x * y
                              def FreeMagma.repr {α : Type u} [Repr α] :

                              Representation of an element of a free magma.

                              Equations
                              Instances For

                                Representation of an element of a free additive magma.

                                Equations
                                Instances For
                                  instance instReprFreeAddMagma {α : Type u} [Repr α] :
                                  Equations
                                  • instReprFreeAddMagma = { reprPrec := fun (o : FreeAddMagma α) (x : ) => o.repr }
                                  instance instReprFreeMagma {α : Type u} [Repr α] :
                                  Equations
                                  • instReprFreeMagma = { reprPrec := fun (o : FreeMagma α) (x : ) => o.repr }
                                  def FreeMagma.length {α : Type u} :
                                  FreeMagma α

                                  Length of an element of a free magma.

                                  Equations
                                  Instances For

                                    Length of an element of a free additive magma.

                                    Equations
                                    Instances For
                                      abbrev FreeAddMagma.length_pos.match_1 {α : Type u_1} (motive : FreeAddMagma αProp) :
                                      ∀ (x : FreeAddMagma α), (∀ (a : α), motive (FreeAddMagma.of a))(∀ (y z : FreeAddMagma α), motive (y.add z))motive x
                                      Equations
                                      • =
                                      Instances For
                                        theorem FreeAddMagma.length_pos {α : Type u} (x : FreeAddMagma α) :
                                        0 < x.length

                                        The length of an element of a free additive magma is positive.

                                        theorem FreeMagma.length_pos {α : Type u} (x : FreeMagma α) :
                                        0 < x.length

                                        The length of an element of a free magma is positive.

                                        inductive AddMagma.AssocRel (α : Type u) [Add α] :
                                        ααProp

                                        Associativity relations for an additive magma.

                                        Instances For
                                          inductive Magma.AssocRel (α : Type u) [Mul α] :
                                          ααProp

                                          Associativity relations for a magma.

                                          Instances For
                                            def AddMagma.FreeAddSemigroup (α : Type u) [Add α] :

                                            Additive semigroup quotient of an additive magma.

                                            Equations
                                            Instances For
                                              def Magma.AssocQuotient (α : Type u) [Mul α] :

                                              Semigroup quotient of a magma.

                                              Equations
                                              Instances For
                                                theorem AddMagma.FreeAddSemigroup.quot_mk_assoc {α : Type u} [Add α] (x : α) (y : α) (z : α) :
                                                Quot.mk (AddMagma.AssocRel α) (x + y + z) = Quot.mk (AddMagma.AssocRel α) (x + (y + z))
                                                theorem Magma.AssocQuotient.quot_mk_assoc {α : Type u} [Mul α] (x : α) (y : α) (z : α) :
                                                Quot.mk (Magma.AssocRel α) (x * y * z) = Quot.mk (Magma.AssocRel α) (x * (y * z))
                                                theorem AddMagma.FreeAddSemigroup.quot_mk_assoc_left {α : Type u} [Add α] (x : α) (y : α) (z : α) (w : α) :
                                                Quot.mk (AddMagma.AssocRel α) (x + (y + z + w)) = Quot.mk (AddMagma.AssocRel α) (x + (y + (z + w)))
                                                theorem Magma.AssocQuotient.quot_mk_assoc_left {α : Type u} [Mul α] (x : α) (y : α) (z : α) (w : α) :
                                                Quot.mk (Magma.AssocRel α) (x * (y * z * w)) = Quot.mk (Magma.AssocRel α) (x * (y * (z * w)))
                                                theorem AddMagma.FreeAddSemigroup.instAddSemigroup.proof_2 {α : Type u_1} [Add α] (a₁ : α) (a₂ : α) (b : α) :
                                                AddMagma.AssocRel α a₁ a₂(fun (x y : α) => Quot.mk (AddMagma.AssocRel α) (x + y)) a₁ b = (fun (x y : α) => Quot.mk (AddMagma.AssocRel α) (x + y)) a₂ b
                                                theorem AddMagma.FreeAddSemigroup.instAddSemigroup.proof_1 {α : Type u_1} [Add α] (a : α) (b₁ : α) (b₂ : α) :
                                                AddMagma.AssocRel α b₁ b₂(fun (x y : α) => Quot.mk (AddMagma.AssocRel α) (x + y)) a b₁ = (fun (x y : α) => Quot.mk (AddMagma.AssocRel α) (x + y)) a b₂
                                                Equations
                                                Equations
                                                theorem AddMagma.FreeAddSemigroup.of.proof_1 {α : Type u_1} [Add α] (_x : α) (_y : α) :

                                                Embedding from additive magma to its free additive semigroup.

                                                Equations
                                                Instances For

                                                  Embedding from magma to its free semigroup.

                                                  Equations
                                                  Instances For
                                                    Equations
                                                    • AddMagma.FreeAddSemigroup.instInhabited = { default := AddMagma.FreeAddSemigroup.of default }
                                                    Equations
                                                    • Magma.AssocQuotient.instInhabited = { default := Magma.AssocQuotient.of default }
                                                    theorem AddMagma.FreeAddSemigroup.induction_on {α : Type u} [Add α] {C : AddMagma.FreeAddSemigroup αProp} (x : AddMagma.FreeAddSemigroup α) (ih : ∀ (x : α), C (AddMagma.FreeAddSemigroup.of x)) :
                                                    C x
                                                    theorem Magma.AssocQuotient.induction_on {α : Type u} [Mul α] {C : Magma.AssocQuotient αProp} (x : Magma.AssocQuotient α) (ih : ∀ (x : α), C (Magma.AssocQuotient.of x)) :
                                                    C x
                                                    theorem AddMagma.FreeAddSemigroup.hom_ext {α : Type u} [Add α] {β : Type v} [AddSemigroup β] {f : AddHom (AddMagma.FreeAddSemigroup α) β} {g : AddHom (AddMagma.FreeAddSemigroup α) β} (h : f.comp AddMagma.FreeAddSemigroup.of = g.comp AddMagma.FreeAddSemigroup.of) :
                                                    f = g
                                                    theorem Magma.AssocQuotient.hom_ext {α : Type u} [Mul α] {β : Type v} [Semigroup β] {f : Magma.AssocQuotient α →ₙ* β} {g : Magma.AssocQuotient α →ₙ* β} (h : f.comp Magma.AssocQuotient.of = g.comp Magma.AssocQuotient.of) :
                                                    f = g
                                                    theorem AddMagma.FreeAddSemigroup.lift.proof_2 {α : Type u_1} [Add α] {β : Type u_2} [AddSemigroup β] (f : AddHom α β) (x : AddMagma.FreeAddSemigroup α) (y : AddMagma.FreeAddSemigroup α) :
                                                    (fun (x : AddMagma.FreeAddSemigroup α) => Quot.liftOn x f ) (x + y) = (fun (x : AddMagma.FreeAddSemigroup α) => Quot.liftOn x f ) x + (fun (x : AddMagma.FreeAddSemigroup α) => Quot.liftOn x f ) y
                                                    theorem AddMagma.FreeAddSemigroup.lift.proof_3 {α : Type u_1} [Add α] {β : Type u_2} [AddSemigroup β] (f : AddHom α β) :
                                                    (fun (f : AddHom (AddMagma.FreeAddSemigroup α) β) => f.comp AddMagma.FreeAddSemigroup.of) ((fun (f : AddHom α β) => { toFun := fun (x : AddMagma.FreeAddSemigroup α) => Quot.liftOn x f , map_add' := }) f) = f
                                                    theorem AddMagma.FreeAddSemigroup.lift.proof_4 {α : Type u_1} [Add α] {β : Type u_2} [AddSemigroup β] (f : AddHom (AddMagma.FreeAddSemigroup α) β) :
                                                    (fun (f : AddHom α β) => { toFun := fun (x : AddMagma.FreeAddSemigroup α) => Quot.liftOn x f , map_add' := }) ((fun (f : AddHom (AddMagma.FreeAddSemigroup α) β) => f.comp AddMagma.FreeAddSemigroup.of) f) = f

                                                    Lifts an additive magma homomorphism α → β to an additive semigroup homomorphism AddMagma.AssocQuotient α → β given an additive semigroup β.

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      theorem AddMagma.FreeAddSemigroup.lift.proof_1 {α : Type u_1} [Add α] {β : Type u_2} [AddSemigroup β] (f : AddHom α β) (a : α) (b : α) :
                                                      AddMagma.AssocRel α a bf a = f b
                                                      @[simp]
                                                      theorem AddMagma.FreeAddSemigroup.lift_symm_apply {α : Type u} [Add α] {β : Type v} [AddSemigroup β] (f : AddHom (AddMagma.FreeAddSemigroup α) β) :
                                                      AddMagma.FreeAddSemigroup.lift.symm f = f.comp AddMagma.FreeAddSemigroup.of
                                                      @[simp]
                                                      theorem Magma.AssocQuotient.lift_symm_apply {α : Type u} [Mul α] {β : Type v} [Semigroup β] (f : Magma.AssocQuotient α →ₙ* β) :
                                                      Magma.AssocQuotient.lift.symm f = f.comp Magma.AssocQuotient.of
                                                      def Magma.AssocQuotient.lift {α : Type u} [Mul α] {β : Type v} [Semigroup β] :

                                                      Lifts a magma homomorphism α → β to a semigroup homomorphism Magma.AssocQuotient α → β given a semigroup β.

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        @[simp]
                                                        theorem AddMagma.FreeAddSemigroup.lift_of {α : Type u} [Add α] {β : Type v} [AddSemigroup β] (f : AddHom α β) (x : α) :
                                                        (AddMagma.FreeAddSemigroup.lift f) (AddMagma.FreeAddSemigroup.of x) = f x
                                                        @[simp]
                                                        theorem Magma.AssocQuotient.lift_of {α : Type u} [Mul α] {β : Type v} [Semigroup β] (f : α →ₙ* β) (x : α) :
                                                        (Magma.AssocQuotient.lift f) (Magma.AssocQuotient.of x) = f x
                                                        @[simp]
                                                        theorem AddMagma.FreeAddSemigroup.lift_comp_of {α : Type u} [Add α] {β : Type v} [AddSemigroup β] (f : AddHom α β) :
                                                        (AddMagma.FreeAddSemigroup.lift f).comp AddMagma.FreeAddSemigroup.of = f
                                                        @[simp]
                                                        theorem Magma.AssocQuotient.lift_comp_of {α : Type u} [Mul α] {β : Type v} [Semigroup β] (f : α →ₙ* β) :
                                                        (Magma.AssocQuotient.lift f).comp Magma.AssocQuotient.of = f
                                                        @[simp]
                                                        theorem AddMagma.FreeAddSemigroup.lift_comp_of' {α : Type u} [Add α] {β : Type v} [AddSemigroup β] (f : AddHom (AddMagma.FreeAddSemigroup α) β) :
                                                        AddMagma.FreeAddSemigroup.lift (f.comp AddMagma.FreeAddSemigroup.of) = f
                                                        @[simp]
                                                        theorem Magma.AssocQuotient.lift_comp_of' {α : Type u} [Mul α] {β : Type v} [Semigroup β] (f : Magma.AssocQuotient α →ₙ* β) :
                                                        Magma.AssocQuotient.lift (f.comp Magma.AssocQuotient.of) = f

                                                        From an additive magma homomorphism α → β to an additive semigroup homomorphism AddMagma.AssocQuotient α → AddMagma.AssocQuotient β.

                                                        Equations
                                                        Instances For

                                                          From a magma homomorphism α →ₙ* β to a semigroup homomorphism Magma.AssocQuotient α →ₙ* Magma.AssocQuotient β.

                                                          Equations
                                                          Instances For
                                                            @[simp]
                                                            theorem AddMagma.FreeAddSemigroup.map_of {α : Type u} [Add α] {β : Type v} [Add β] (f : AddHom α β) (x : α) :
                                                            (AddMagma.FreeAddSemigroup.map f) (AddMagma.FreeAddSemigroup.of x) = AddMagma.FreeAddSemigroup.of (f x)
                                                            @[simp]
                                                            theorem Magma.AssocQuotient.map_of {α : Type u} [Mul α] {β : Type v} [Mul β] (f : α →ₙ* β) (x : α) :
                                                            (Magma.AssocQuotient.map f) (Magma.AssocQuotient.of x) = Magma.AssocQuotient.of (f x)
                                                            structure FreeAddSemigroup (α : Type u) :

                                                            Free additive semigroup over a given alphabet.

                                                            • head : α

                                                              The head of the element

                                                            • tail : List α

                                                              The tail of the element

                                                            Instances For
                                                              theorem FreeSemigroup.ext_iff {α : Type u} (x : FreeSemigroup α) (y : FreeSemigroup α) :
                                                              x = y x.head = y.head x.tail = y.tail
                                                              theorem FreeAddSemigroup.ext {α : Type u} (x : FreeAddSemigroup α) (y : FreeAddSemigroup α) (head : x.head = y.head) (tail : x.tail = y.tail) :
                                                              x = y
                                                              theorem FreeAddSemigroup.ext_iff {α : Type u} (x : FreeAddSemigroup α) (y : FreeAddSemigroup α) :
                                                              x = y x.head = y.head x.tail = y.tail
                                                              theorem FreeSemigroup.ext {α : Type u} (x : FreeSemigroup α) (y : FreeSemigroup α) (head : x.head = y.head) (tail : x.tail = y.tail) :
                                                              x = y
                                                              structure FreeSemigroup (α : Type u) :

                                                              Free semigroup over a given alphabet.

                                                              • head : α

                                                                The head of the element

                                                              • tail : List α

                                                                The tail of the element

                                                              Instances For
                                                                theorem FreeAddSemigroup.instAddSemigroup.proof_1 {α : Type u_1} (_L1 : FreeAddSemigroup α) (_L2 : FreeAddSemigroup α) (_L3 : FreeAddSemigroup α) :
                                                                _L1 + _L2 + _L3 = _L1 + (_L2 + _L3)
                                                                Equations
                                                                Equations
                                                                @[simp]
                                                                theorem FreeAddSemigroup.head_add {α : Type u} (x : FreeAddSemigroup α) (y : FreeAddSemigroup α) :
                                                                (x + y).head = x.head
                                                                @[simp]
                                                                theorem FreeSemigroup.head_mul {α : Type u} (x : FreeSemigroup α) (y : FreeSemigroup α) :
                                                                (x * y).head = x.head
                                                                @[simp]
                                                                theorem FreeAddSemigroup.tail_add {α : Type u} (x : FreeAddSemigroup α) (y : FreeAddSemigroup α) :
                                                                (x + y).tail = x.tail ++ y.head :: y.tail
                                                                @[simp]
                                                                theorem FreeSemigroup.tail_mul {α : Type u} (x : FreeSemigroup α) (y : FreeSemigroup α) :
                                                                (x * y).tail = x.tail ++ y.head :: y.tail
                                                                @[simp]
                                                                theorem FreeAddSemigroup.mk_add_mk {α : Type u} (x : α) (y : α) (L1 : List α) (L2 : List α) :
                                                                { head := x, tail := L1 } + { head := y, tail := L2 } = { head := x, tail := L1 ++ y :: L2 }
                                                                @[simp]
                                                                theorem FreeSemigroup.mk_mul_mk {α : Type u} (x : α) (y : α) (L1 : List α) (L2 : List α) :
                                                                { head := x, tail := L1 } * { head := y, tail := L2 } = { head := x, tail := L1 ++ y :: L2 }
                                                                def FreeAddSemigroup.of {α : Type u} (x : α) :

                                                                The embedding α → FreeAddSemigroup α.

                                                                Equations
                                                                Instances For
                                                                  @[simp]
                                                                  theorem FreeAddSemigroup.of_tail {α : Type u} (x : α) :
                                                                  @[simp]
                                                                  theorem FreeSemigroup.of_head {α : Type u} (x : α) :
                                                                  (FreeSemigroup.of x).head = x
                                                                  @[simp]
                                                                  theorem FreeAddSemigroup.of_head {α : Type u} (x : α) :
                                                                  @[simp]
                                                                  theorem FreeSemigroup.of_tail {α : Type u} (x : α) :
                                                                  (FreeSemigroup.of x).tail = []
                                                                  def FreeSemigroup.of {α : Type u} (x : α) :

                                                                  The embedding α → FreeSemigroup α.

                                                                  Equations
                                                                  Instances For

                                                                    Length of an element of free additive semigroup

                                                                    Equations
                                                                    • x.length = x.tail.length + 1
                                                                    Instances For

                                                                      Length of an element of free semigroup.

                                                                      Equations
                                                                      • x.length = x.tail.length + 1
                                                                      Instances For
                                                                        @[simp]
                                                                        theorem FreeAddSemigroup.length_add {α : Type u} (x : FreeAddSemigroup α) (y : FreeAddSemigroup α) :
                                                                        (x + y).length = x.length + y.length
                                                                        @[simp]
                                                                        theorem FreeSemigroup.length_mul {α : Type u} (x : FreeSemigroup α) (y : FreeSemigroup α) :
                                                                        (x * y).length = x.length + y.length
                                                                        @[simp]
                                                                        theorem FreeAddSemigroup.length_of {α : Type u} (x : α) :
                                                                        (FreeAddSemigroup.of x).length = 1
                                                                        @[simp]
                                                                        theorem FreeSemigroup.length_of {α : Type u} (x : α) :
                                                                        (FreeSemigroup.of x).length = 1
                                                                        Equations
                                                                        Equations
                                                                        def FreeAddSemigroup.recOnAdd {α : Type u} {C : FreeAddSemigroup αSort l} (x : FreeAddSemigroup α) (ih1 : (x : α) → C (FreeAddSemigroup.of x)) (ih2 : (x : α) → (y : FreeAddSemigroup α) → C (FreeAddSemigroup.of x)C yC (FreeAddSemigroup.of x + y)) :
                                                                        C x

                                                                        Recursor for free additive semigroup using of and +.

                                                                        Equations
                                                                        • One or more equations did not get rendered due to their size.
                                                                        Instances For
                                                                          def FreeSemigroup.recOnMul {α : Type u} {C : FreeSemigroup αSort l} (x : FreeSemigroup α) (ih1 : (x : α) → C (FreeSemigroup.of x)) (ih2 : (x : α) → (y : FreeSemigroup α) → C (FreeSemigroup.of x)C yC (FreeSemigroup.of x * y)) :
                                                                          C x

                                                                          Recursor for free semigroup using of and *.

                                                                          Equations
                                                                          • One or more equations did not get rendered due to their size.
                                                                          Instances For
                                                                            theorem FreeAddSemigroup.hom_ext {α : Type u} {β : Type v} [Add β] {f : AddHom (FreeAddSemigroup α) β} {g : AddHom (FreeAddSemigroup α) β} (h : f FreeAddSemigroup.of = g FreeAddSemigroup.of) :
                                                                            f = g
                                                                            theorem FreeSemigroup.hom_ext {α : Type u} {β : Type v} [Mul β] {f : FreeSemigroup α →ₙ* β} {g : FreeSemigroup α →ₙ* β} (h : f FreeSemigroup.of = g FreeSemigroup.of) :
                                                                            f = g
                                                                            theorem FreeAddSemigroup.lift.proof_3 {α : Type u_1} {β : Type u_2} [AddSemigroup β] (f : AddHom (FreeAddSemigroup α) β) :
                                                                            (fun (f : αβ) => { toFun := fun (x : FreeAddSemigroup α) => List.foldl (fun (a : β) (b : α) => a + f b) (f x.head) x.tail, map_add' := }) ((fun (f : AddHom (FreeAddSemigroup α) β) => f FreeAddSemigroup.of) f) = f
                                                                            def FreeAddSemigroup.lift {α : Type u} {β : Type v} [AddSemigroup β] :
                                                                            (αβ) AddHom (FreeAddSemigroup α) β

                                                                            Lifts a function α → β to an additive semigroup homomorphism FreeAddSemigroup α → β given an additive semigroup β.

                                                                            Equations
                                                                            • One or more equations did not get rendered due to their size.
                                                                            Instances For
                                                                              theorem FreeAddSemigroup.lift.proof_2 {α : Type u_1} {β : Type u_2} [AddSemigroup β] (f : αβ) :
                                                                              (fun (f : AddHom (FreeAddSemigroup α) β) => f FreeAddSemigroup.of) ((fun (f : αβ) => { toFun := fun (x : FreeAddSemigroup α) => List.foldl (fun (a : β) (b : α) => a + f b) (f x.head) x.tail, map_add' := }) f) = (fun (f : AddHom (FreeAddSemigroup α) β) => f FreeAddSemigroup.of) ((fun (f : αβ) => { toFun := fun (x : FreeAddSemigroup α) => List.foldl (fun (a : β) (b : α) => a + f b) (f x.head) x.tail, map_add' := }) f)
                                                                              theorem FreeAddSemigroup.lift.proof_1 {α : Type u_1} {β : Type u_2} [AddSemigroup β] (f : αβ) (x : FreeAddSemigroup α) (y : FreeAddSemigroup α) :
                                                                              List.foldl (fun (a : β) (b : α) => a + f b) (f x.head) (x.tail ++ y.head :: y.tail) = List.foldl (fun (x : β) (y : α) => x + f y) (f x.head) x.tail + List.foldl (fun (x : β) (y : α) => x + f y) (f y.head) y.tail
                                                                              @[simp]
                                                                              theorem FreeSemigroup.lift_symm_apply {α : Type u} {β : Type v} [Semigroup β] (f : FreeSemigroup α →ₙ* β) :
                                                                              ∀ (a : α), FreeSemigroup.lift.symm f a = (f FreeSemigroup.of) a
                                                                              @[simp]
                                                                              theorem FreeAddSemigroup.lift_symm_apply {α : Type u} {β : Type v} [AddSemigroup β] (f : AddHom (FreeAddSemigroup α) β) :
                                                                              ∀ (a : α), FreeAddSemigroup.lift.symm f a = (f FreeAddSemigroup.of) a
                                                                              def FreeSemigroup.lift {α : Type u} {β : Type v} [Semigroup β] :
                                                                              (αβ) (FreeSemigroup α →ₙ* β)

                                                                              Lifts a function α → β to a semigroup homomorphism FreeSemigroup α → β given a semigroup β.

                                                                              Equations
                                                                              • One or more equations did not get rendered due to their size.
                                                                              Instances For
                                                                                @[simp]
                                                                                theorem FreeAddSemigroup.lift_of {α : Type u} {β : Type v} [AddSemigroup β] (f : αβ) (x : α) :
                                                                                (FreeAddSemigroup.lift f) (FreeAddSemigroup.of x) = f x
                                                                                @[simp]
                                                                                theorem FreeSemigroup.lift_of {α : Type u} {β : Type v} [Semigroup β] (f : αβ) (x : α) :
                                                                                (FreeSemigroup.lift f) (FreeSemigroup.of x) = f x
                                                                                @[simp]
                                                                                theorem FreeAddSemigroup.lift_comp_of {α : Type u} {β : Type v} [AddSemigroup β] (f : αβ) :
                                                                                (FreeAddSemigroup.lift f) FreeAddSemigroup.of = f
                                                                                @[simp]
                                                                                theorem FreeSemigroup.lift_comp_of {α : Type u} {β : Type v} [Semigroup β] (f : αβ) :
                                                                                (FreeSemigroup.lift f) FreeSemigroup.of = f
                                                                                @[simp]
                                                                                theorem FreeAddSemigroup.lift_comp_of' {α : Type u} {β : Type v} [AddSemigroup β] (f : AddHom (FreeAddSemigroup α) β) :
                                                                                FreeAddSemigroup.lift (f FreeAddSemigroup.of) = f
                                                                                @[simp]
                                                                                theorem FreeSemigroup.lift_comp_of' {α : Type u} {β : Type v} [Semigroup β] (f : FreeSemigroup α →ₙ* β) :
                                                                                FreeSemigroup.lift (f FreeSemigroup.of) = f
                                                                                theorem FreeAddSemigroup.lift_of_add {α : Type u} {β : Type v} [AddSemigroup β] (f : αβ) (x : α) (y : FreeAddSemigroup α) :
                                                                                (FreeAddSemigroup.lift f) (FreeAddSemigroup.of x + y) = f x + (FreeAddSemigroup.lift f) y
                                                                                theorem FreeSemigroup.lift_of_mul {α : Type u} {β : Type v} [Semigroup β] (f : αβ) (x : α) (y : FreeSemigroup α) :
                                                                                (FreeSemigroup.lift f) (FreeSemigroup.of x * y) = f x * (FreeSemigroup.lift f) y
                                                                                def FreeAddSemigroup.map {α : Type u} {β : Type v} (f : αβ) :

                                                                                The unique additive semigroup homomorphism that sends of x to of (f x).

                                                                                Equations
                                                                                Instances For
                                                                                  def FreeSemigroup.map {α : Type u} {β : Type v} (f : αβ) :

                                                                                  The unique semigroup homomorphism that sends of x to of (f x).

                                                                                  Equations
                                                                                  Instances For
                                                                                    @[simp]
                                                                                    theorem FreeAddSemigroup.map_of {α : Type u} {β : Type v} (f : αβ) (x : α) :
                                                                                    @[simp]
                                                                                    theorem FreeSemigroup.map_of {α : Type u} {β : Type v} (f : αβ) (x : α) :
                                                                                    @[simp]
                                                                                    theorem FreeAddSemigroup.length_map {α : Type u} {β : Type v} (f : αβ) (x : FreeAddSemigroup α) :
                                                                                    ((FreeAddSemigroup.map f) x).length = x.length
                                                                                    @[simp]
                                                                                    theorem FreeSemigroup.length_map {α : Type u} {β : Type v} (f : αβ) (x : FreeSemigroup α) :
                                                                                    ((FreeSemigroup.map f) x).length = x.length
                                                                                    def FreeAddSemigroup.recOnPure {α : Type u} {C : FreeAddSemigroup αSort l} (x : FreeAddSemigroup α) (ih1 : (x : α) → C (pure x)) (ih2 : (x : α) → (y : FreeAddSemigroup α) → C (pure x)C yC (pure x + y)) :
                                                                                    C x

                                                                                    Recursor that uses pure instead of of.

                                                                                    Equations
                                                                                    • x.recOnPure ih1 ih2 = x.recOnAdd ih1 ih2
                                                                                    Instances For
                                                                                      def FreeSemigroup.recOnPure {α : Type u} {C : FreeSemigroup αSort l} (x : FreeSemigroup α) (ih1 : (x : α) → C (pure x)) (ih2 : (x : α) → (y : FreeSemigroup α) → C (pure x)C yC (pure x * y)) :
                                                                                      C x

                                                                                      Recursor that uses pure instead of of.

                                                                                      Equations
                                                                                      • x.recOnPure ih1 ih2 = x.recOnMul ih1 ih2
                                                                                      Instances For
                                                                                        @[simp]
                                                                                        theorem FreeAddSemigroup.map_pure {α : Type u} {β : Type u} (f : αβ) (x : α) :
                                                                                        f <$> pure x = pure (f x)
                                                                                        @[simp]
                                                                                        theorem FreeSemigroup.map_pure {α : Type u} {β : Type u} (f : αβ) (x : α) :
                                                                                        f <$> pure x = pure (f x)
                                                                                        @[simp]
                                                                                        theorem FreeAddSemigroup.map_add' {α : Type u} {β : Type u} (f : αβ) (x : FreeAddSemigroup α) (y : FreeAddSemigroup α) :
                                                                                        f <$> (x + y) = f <$> x + f <$> y
                                                                                        @[simp]
                                                                                        theorem FreeSemigroup.map_mul' {α : Type u} {β : Type u} (f : αβ) (x : FreeSemigroup α) (y : FreeSemigroup α) :
                                                                                        f <$> (x * y) = f <$> x * f <$> y
                                                                                        @[simp]
                                                                                        theorem FreeAddSemigroup.pure_bind {α : Type u} {β : Type u} (f : αFreeAddSemigroup β) (x : α) :
                                                                                        pure x >>= f = f x
                                                                                        @[simp]
                                                                                        theorem FreeSemigroup.pure_bind {α : Type u} {β : Type u} (f : αFreeSemigroup β) (x : α) :
                                                                                        pure x >>= f = f x
                                                                                        @[simp]
                                                                                        theorem FreeAddSemigroup.add_bind {α : Type u} {β : Type u} (f : αFreeAddSemigroup β) (x : FreeAddSemigroup α) (y : FreeAddSemigroup α) :
                                                                                        x + y >>= f = (x >>= f) + (y >>= f)
                                                                                        @[simp]
                                                                                        theorem FreeSemigroup.mul_bind {α : Type u} {β : Type u} (f : αFreeSemigroup β) (x : FreeSemigroup α) (y : FreeSemigroup α) :
                                                                                        x * y >>= f = (x >>= f) * (y >>= f)
                                                                                        @[simp]
                                                                                        theorem FreeAddSemigroup.pure_seq {α : Type u} {β : Type u} {f : αβ} {x : FreeAddSemigroup α} :
                                                                                        (Seq.seq (pure f) fun (x_1 : Unit) => x) = f <$> x
                                                                                        @[simp]
                                                                                        theorem FreeSemigroup.pure_seq {α : Type u} {β : Type u} {f : αβ} {x : FreeSemigroup α} :
                                                                                        (Seq.seq (pure f) fun (x_1 : Unit) => x) = f <$> x
                                                                                        @[simp]
                                                                                        theorem FreeAddSemigroup.add_seq {α : Type u} {β : Type u} {f : FreeAddSemigroup (αβ)} {g : FreeAddSemigroup (αβ)} {x : FreeAddSemigroup α} :
                                                                                        (Seq.seq (f + g) fun (x_1 : Unit) => x) = (Seq.seq f fun (x_1 : Unit) => x) + Seq.seq g fun (x_1 : Unit) => x
                                                                                        @[simp]
                                                                                        theorem FreeSemigroup.mul_seq {α : Type u} {β : Type u} {f : FreeSemigroup (αβ)} {g : FreeSemigroup (αβ)} {x : FreeSemigroup α} :
                                                                                        (Seq.seq (f * g) fun (x_1 : Unit) => x) = (Seq.seq f fun (x_1 : Unit) => x) * Seq.seq g fun (x_1 : Unit) => x
                                                                                        def FreeAddSemigroup.traverse {m : Type u → Type u} [Applicative m] {α : Type u} {β : Type u} (F : αm β) (x : FreeAddSemigroup α) :

                                                                                        FreeAddSemigroup is traversable.

                                                                                        Equations
                                                                                        • One or more equations did not get rendered due to their size.
                                                                                        Instances For
                                                                                          def FreeSemigroup.traverse {m : Type u → Type u} [Applicative m] {α : Type u} {β : Type u} (F : αm β) (x : FreeSemigroup α) :

                                                                                          FreeSemigroup is traversable.

                                                                                          Equations
                                                                                          • One or more equations did not get rendered due to their size.
                                                                                          Instances For
                                                                                            @[simp]
                                                                                            theorem FreeAddSemigroup.traverse_pure {α : Type u} {β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) (x : α) :
                                                                                            traverse F (pure x) = pure <$> F x
                                                                                            @[simp]
                                                                                            theorem FreeSemigroup.traverse_pure {α : Type u} {β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) (x : α) :
                                                                                            traverse F (pure x) = pure <$> F x
                                                                                            @[simp]
                                                                                            theorem FreeAddSemigroup.traverse_pure' {α : Type u} {β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) :
                                                                                            traverse F pure = fun (x : α) => pure <$> F x
                                                                                            @[simp]
                                                                                            theorem FreeSemigroup.traverse_pure' {α : Type u} {β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) :
                                                                                            traverse F pure = fun (x : α) => pure <$> F x
                                                                                            @[simp]
                                                                                            theorem FreeAddSemigroup.traverse_add {α : Type u} {β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) [LawfulApplicative m] (x : FreeAddSemigroup α) (y : FreeAddSemigroup α) :
                                                                                            traverse F (x + y) = Seq.seq ((fun (x x_1 : FreeAddSemigroup β) => x + x_1) <$> traverse F x) fun (x : Unit) => traverse F y
                                                                                            @[simp]
                                                                                            theorem FreeSemigroup.traverse_mul {α : Type u} {β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) [LawfulApplicative m] (x : FreeSemigroup α) (y : FreeSemigroup α) :
                                                                                            traverse F (x * y) = Seq.seq ((fun (x x_1 : FreeSemigroup β) => x * x_1) <$> traverse F x) fun (x : Unit) => traverse F y
                                                                                            @[simp]
                                                                                            theorem FreeAddSemigroup.traverse_add' {α : Type u} {β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) [LawfulApplicative m] :
                                                                                            Function.comp (traverse F) HAdd.hAdd = fun (x y : FreeAddSemigroup α) => Seq.seq ((fun (x x_1 : FreeAddSemigroup β) => x + x_1) <$> traverse F x) fun (x : Unit) => traverse F y
                                                                                            @[simp]
                                                                                            theorem FreeSemigroup.traverse_mul' {α : Type u} {β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) [LawfulApplicative m] :
                                                                                            Function.comp (traverse F) HMul.hMul = fun (x y : FreeSemigroup α) => Seq.seq ((fun (x x_1 : FreeSemigroup β) => x * x_1) <$> traverse F x) fun (x : Unit) => traverse F y
                                                                                            @[simp]
                                                                                            theorem FreeAddSemigroup.traverse_eq {α : Type u} {β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) (x : FreeAddSemigroup α) :
                                                                                            @[simp]
                                                                                            theorem FreeSemigroup.traverse_eq {α : Type u} {β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) (x : FreeSemigroup α) :
                                                                                            @[simp]
                                                                                            theorem FreeAddSemigroup.add_map_seq {α : Type u} (x : FreeAddSemigroup α) (y : FreeAddSemigroup α) :
                                                                                            (Seq.seq ((fun (x x_1 : FreeAddSemigroup α) => x + x_1) <$> x) fun (x : Unit) => y) = x + y
                                                                                            @[simp]
                                                                                            theorem FreeSemigroup.mul_map_seq {α : Type u} (x : FreeSemigroup α) (y : FreeSemigroup α) :
                                                                                            (Seq.seq ((fun (x x_1 : FreeSemigroup α) => x * x_1) <$> x) fun (x : Unit) => y) = x * y
                                                                                            Equations
                                                                                            Equations

                                                                                            The canonical additive morphism from FreeAddMagma α to FreeAddSemigroup α.

                                                                                            Equations
                                                                                            • FreeAddMagma.toFreeAddSemigroup = FreeAddMagma.lift FreeAddSemigroup.of
                                                                                            Instances For

                                                                                              The canonical multiplicative morphism from FreeMagma α to FreeSemigroup α.

                                                                                              Equations
                                                                                              • FreeMagma.toFreeSemigroup = FreeMagma.lift FreeSemigroup.of
                                                                                              Instances For
                                                                                                @[simp]
                                                                                                theorem FreeAddMagma.toFreeAddSemigroup_of {α : Type u} (x : α) :
                                                                                                FreeAddMagma.toFreeAddSemigroup (FreeAddMagma.of x) = FreeAddSemigroup.of x
                                                                                                @[simp]
                                                                                                theorem FreeMagma.toFreeSemigroup_of {α : Type u} (x : α) :
                                                                                                FreeMagma.toFreeSemigroup (FreeMagma.of x) = FreeSemigroup.of x
                                                                                                @[simp]
                                                                                                theorem FreeAddMagma.toFreeAddSemigroup_comp_of {α : Type u} :
                                                                                                FreeAddMagma.toFreeAddSemigroup FreeAddMagma.of = FreeAddSemigroup.of
                                                                                                @[simp]
                                                                                                theorem FreeMagma.toFreeSemigroup_comp_of {α : Type u} :
                                                                                                FreeMagma.toFreeSemigroup FreeMagma.of = FreeSemigroup.of
                                                                                                theorem FreeAddMagma.toFreeAddSemigroup_comp_map {α : Type u} {β : Type v} (f : αβ) :
                                                                                                FreeAddMagma.toFreeAddSemigroup.comp (FreeAddMagma.map f) = (FreeAddSemigroup.map f).comp FreeAddMagma.toFreeAddSemigroup
                                                                                                theorem FreeMagma.toFreeSemigroup_comp_map {α : Type u} {β : Type v} (f : αβ) :
                                                                                                FreeMagma.toFreeSemigroup.comp (FreeMagma.map f) = (FreeSemigroup.map f).comp FreeMagma.toFreeSemigroup
                                                                                                theorem FreeAddMagma.toFreeAddSemigroup_map {α : Type u} {β : Type v} (f : αβ) (x : FreeAddMagma α) :
                                                                                                FreeAddMagma.toFreeAddSemigroup ((FreeAddMagma.map f) x) = (FreeAddSemigroup.map f) (FreeAddMagma.toFreeAddSemigroup x)
                                                                                                theorem FreeMagma.toFreeSemigroup_map {α : Type u} {β : Type v} (f : αβ) (x : FreeMagma α) :
                                                                                                FreeMagma.toFreeSemigroup ((FreeMagma.map f) x) = (FreeSemigroup.map f) (FreeMagma.toFreeSemigroup x)
                                                                                                @[simp]
                                                                                                theorem FreeAddMagma.length_toFreeAddSemigroup {α : Type u} (x : FreeAddMagma α) :
                                                                                                (FreeAddMagma.toFreeAddSemigroup x).length = x.length
                                                                                                @[simp]
                                                                                                theorem FreeMagma.length_toFreeSemigroup {α : Type u} (x : FreeMagma α) :
                                                                                                (FreeMagma.toFreeSemigroup x).length = x.length

                                                                                                Isomorphism between AddMagma.AssocQuotient (FreeAddMagma α) and FreeAddSemigroup α.

                                                                                                Equations
                                                                                                • FreeAddMagmaAssocQuotientEquiv α = (AddMagma.FreeAddSemigroup.lift FreeAddMagma.toFreeAddSemigroup).toAddEquiv (FreeAddSemigroup.lift (AddMagma.FreeAddSemigroup.of FreeAddMagma.of))
                                                                                                Instances For
                                                                                                  theorem FreeAddMagmaAssocQuotientEquiv.proof_1 (α : Type u_1) :
                                                                                                  (FreeAddSemigroup.lift (AddMagma.FreeAddSemigroup.of FreeAddMagma.of)).comp (AddMagma.FreeAddSemigroup.lift FreeAddMagma.toFreeAddSemigroup) = AddHom.id (AddMagma.FreeAddSemigroup (FreeAddMagma α))
                                                                                                  theorem FreeAddMagmaAssocQuotientEquiv.proof_2 (α : Type u_1) :
                                                                                                  (AddMagma.FreeAddSemigroup.lift FreeAddMagma.toFreeAddSemigroup).comp (FreeAddSemigroup.lift (AddMagma.FreeAddSemigroup.of FreeAddMagma.of)) = AddHom.id (FreeAddSemigroup α)

                                                                                                  Isomorphism between Magma.AssocQuotient (FreeMagma α) and FreeSemigroup α.

                                                                                                  Equations
                                                                                                  • FreeMagmaAssocQuotientEquiv α = (Magma.AssocQuotient.lift FreeMagma.toFreeSemigroup).toMulEquiv (FreeSemigroup.lift (Magma.AssocQuotient.of FreeMagma.of))
                                                                                                  Instances For