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
      • FreeMagma.instInhabitedFreeMagma = { default := FreeMagma.of default }
      Equations
      • FreeAddMagma.instAddFreeAddMagma = { add := FreeAddMagma.add }
      Equations
      • FreeMagma.instMulFreeMagma = { mul := FreeMagma.mul }
      @[simp]
      theorem FreeAddMagma.add_eq {α : Type u} (x : FreeAddMagma α) (y : FreeAddMagma α) :
      @[simp]
      theorem FreeMagma.mul_eq {α : Type u} (x : FreeMagma α) (y : FreeMagma α) :
      FreeMagma.mul x y = x * y
      noncomputable 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
      noncomputable 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
      theorem FreeAddMagma.hom_ext {α : Type u} {β : Type v} [inst : Add β] {f : AddHom (FreeAddMagma α) β} {g : AddHom (FreeAddMagma α) β} (h : f FreeAddMagma.of = g FreeAddMagma.of) :
      f = g
      theorem FreeMagma.hom_ext {α : Type u} {β : Type v} [inst : Mul β] {f : FreeMagma α →ₙ* β} {g : FreeMagma α →ₙ* β} (h : f FreeMagma.of = g FreeMagma.of) :
      f = g
      def FreeMagma.liftAux {α : Type u} {β : Type v} [inst : Mul β] (f : αβ) :
      FreeMagma αβ

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

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

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

      Equations
      def FreeAddMagma.lift.proof_2 {α : Type u_1} {β : Type u_2} [inst : Add β] (f : αβ) :
      (fun F => F FreeAddMagma.of) ((fun f => { toFun := FreeAddMagma.liftAux f, map_add' := (_ : ∀ (x y : FreeAddMagma α), FreeAddMagma.liftAux f (x + y) = FreeAddMagma.liftAux f (x + y)) }) f) = (fun F => F FreeAddMagma.of) ((fun f => { toFun := FreeAddMagma.liftAux f, map_add' := (_ : ∀ (x y : FreeAddMagma α), FreeAddMagma.liftAux f (x + y) = FreeAddMagma.liftAux f (x + y)) }) f)
      Equations
      • One or more equations did not get rendered due to their size.
      def FreeAddMagma.lift {α : Type u} {β : Type v} [inst : 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.
      def FreeAddMagma.lift.proof_1 {α : Type u_1} {β : Type u_2} [inst : Add β] (f : αβ) (x : FreeAddMagma α) (y : FreeAddMagma α) :
      Equations
      def FreeAddMagma.lift.proof_3 {α : Type u_1} {β : Type u_2} [inst : Add β] (F : AddHom (FreeAddMagma α) β) :
      (fun f => { toFun := FreeAddMagma.liftAux f, map_add' := (_ : ∀ (x y : FreeAddMagma α), FreeAddMagma.liftAux f (x + y) = FreeAddMagma.liftAux f (x + y)) }) ((fun F => F FreeAddMagma.of) F) = F
      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem FreeAddMagma.lift_symm_apply {α : Type u} {β : Type v} [inst : Add β] (F : AddHom (FreeAddMagma α) β) :
      ∀ (a : α), ↑(Equiv.symm FreeAddMagma.lift) F a = (F FreeAddMagma.of) a
      @[simp]
      theorem FreeMagma.lift_symm_apply {α : Type u} {β : Type v} [inst : Mul β] (F : FreeMagma α →ₙ* β) :
      ∀ (a : α), ↑(Equiv.symm FreeMagma.lift) F a = (F FreeMagma.of) a
      def FreeMagma.lift {α : Type u} {β : Type v} [inst : Mul β] :
      (αβ) (FreeMagma α →ₙ* β)

      The universal property of the free magma expressing its adjointness.

      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem FreeAddMagma.lift_of {α : Type u} {β : Type v} [inst : Add β] (f : αβ) (x : α) :
      ↑(FreeAddMagma.lift f) (FreeAddMagma.of x) = f x
      @[simp]
      theorem FreeMagma.lift_of {α : Type u} {β : Type v} [inst : Mul β] (f : αβ) (x : α) :
      ↑(FreeMagma.lift f) (FreeMagma.of x) = f x
      @[simp]
      theorem FreeAddMagma.lift_comp_of {α : Type u} {β : Type v} [inst : Add β] (f : αβ) :
      ↑(FreeAddMagma.lift f) FreeAddMagma.of = f
      @[simp]
      theorem FreeMagma.lift_comp_of {α : Type u} {β : Type v} [inst : Mul β] (f : αβ) :
      ↑(FreeMagma.lift f) FreeMagma.of = f
      @[simp]
      theorem FreeAddMagma.lift_comp_of' {α : Type u} {β : Type v} [inst : Add β] (f : AddHom (FreeAddMagma α) β) :
      FreeAddMagma.lift (f FreeAddMagma.of) = f
      @[simp]
      theorem FreeMagma.lift_comp_of' {α : Type u} {β : Type v} [inst : Mul β] (f : FreeMagma α →ₙ* β) :
      FreeMagma.lift (f FreeMagma.of) = f
      def FreeAddMagma.map {α : Type u} {β : Type v} (f : αβ) :

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

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

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

      Equations
      @[simp]
      theorem FreeAddMagma.map_of {α : Type u} {β : Type v} (f : αβ) (x : α) :
      @[simp]
      theorem FreeMagma.map_of {α : Type u} {β : Type v} (f : αβ) (x : α) :
      noncomputable 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
      noncomputable 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
      @[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 => x) = f <$> x
      @[simp]
      theorem FreeMagma.pure_seq {α : Type u} {β : Type u} {f : αβ} {x : FreeMagma α} :
      (Seq.seq (pure f) fun x => x) = f <$> x
      @[simp]
      theorem FreeAddMagma.add_seq {α : Type u} {β : Type u} {f : FreeAddMagma (αβ)} {g : FreeAddMagma (αβ)} {x : FreeAddMagma α} :
      (Seq.seq (f + g) fun x => x) = (Seq.seq f fun x => x) + Seq.seq g fun x => x
      @[simp]
      theorem FreeMagma.mul_seq {α : Type u} {β : Type u} {f : FreeMagma (αβ)} {g : FreeMagma (αβ)} {x : FreeMagma α} :
      (Seq.seq (f * g) fun x => x) = (Seq.seq f fun x => x) * Seq.seq g fun x => x
      def FreeMagma.traverse {m : Type u → Type u} [inst : Applicative m] {α : Type u} {β : Type u} (F : αm β) :
      FreeMagma αm (FreeMagma β)

      FreeMagma is traversable.

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

      FreeAddMagma is traversable.

      Equations
      @[simp]
      theorem FreeAddMagma.traverse_pure {α : Type u} {β : Type u} {m : Type u → Type u} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : Applicative m] (F : αm β) (x : FreeAddMagma α) (y : FreeAddMagma α) :
      traverse F (x + y) = Seq.seq ((fun x x_1 => x + x_1) <$> traverse F x) fun x => traverse F y
      @[simp]
      theorem FreeMagma.traverse_mul {α : Type u} {β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : αm β) (x : FreeMagma α) (y : FreeMagma α) :
      traverse F (x * y) = Seq.seq ((fun x x_1 => x * x_1) <$> traverse F x) fun x => traverse F y
      @[simp]
      theorem FreeAddMagma.traverse_add' {α : Type u} {β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : αm β) :
      Function.comp (traverse F) Add.add = fun x y => Seq.seq ((fun x x_1 => x + x_1) <$> traverse F x) fun x => traverse F y
      @[simp]
      theorem FreeMagma.traverse_mul' {α : Type u} {β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : αm β) :
      Function.comp (traverse F) Mul.mul = fun x y => Seq.seq ((fun x x_1 => x * x_1) <$> traverse F x) fun x => traverse F y
      @[simp]
      theorem FreeAddMagma.traverse_eq {α : Type u} {β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : αm β) (x : FreeAddMagma α) :
      @[simp]
      theorem FreeMagma.traverse_eq {α : Type u} {β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : αm β) (x : FreeMagma α) :
      @[simp]
      theorem FreeAddMagma.add_map_seq {α : Type u} (x : FreeAddMagma α) (y : FreeAddMagma α) :
      (Seq.seq ((fun x x_1 => x + x_1) <$> x) fun x => y) = x + y
      @[simp]
      theorem FreeMagma.mul_map_seq {α : Type u} (x : FreeMagma α) (y : FreeMagma α) :
      (Seq.seq ((fun x x_1 => x * x_1) <$> x) fun x => y) = x * y
      Equations
      • One or more equations did not get rendered due to their size.
      def FreeAddMagma.instIsLawfulTraversableFreeAddMagmaInstTraversableFreeAddMagma.proof_5 :
      ∀ {F G : Type u_1 → Type u_1} [inst : Applicative F] [inst_1 : Applicative G] [inst_2 : LawfulApplicative F] [inst_3 : LawfulApplicative G] (η : ApplicativeTransformation F G) (α β : Type u_1) (f : αF β) (x : FreeAddMagma α), (fun {α} => ApplicativeTransformation.app η α) (traverse f x) = traverse ((fun {α} => ApplicativeTransformation.app η α) f) x
      Equations
      • One or more equations did not get rendered due to their size.
      Equations
      def FreeAddMagma.instIsLawfulTraversableFreeAddMagmaInstTraversableFreeAddMagma.proof_3 :
      ∀ {F G : Type u_1 → Type u_1} [inst : Applicative F] [inst_1 : Applicative G] [inst_2 : LawfulApplicative F] [inst_3 : LawfulApplicative G] {α β γ : Type u_1} (f : βF γ) (g : αG β) (x : FreeAddMagma α), traverse (Functor.Comp.mk Functor.map f g) x = Functor.Comp.mk (traverse f <$> traverse g x)
      Equations
      • One or more equations did not get rendered due to their size.
      Equations
      • One or more equations did not get rendered due to their size.
      def FreeMagma.repr {α : Type u} [inst : Repr α] :

      Representation of an element of a free magma.

      Equations
      def FreeAddMagma.repr {α : Type u} [inst : Repr α] :

      Representation of an element of a free additive magma.

      Equations
      instance instReprFreeAddMagma {α : Type u} [inst : Repr α] :
      Equations
      instance instReprFreeMagma {α : Type u} [inst : Repr α] :
      Equations
      def FreeMagma.length {α : Type u} :
      FreeMagma α

      Length of an element of a free magma.

      Equations

      Length of an element of a free additive magma.

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

      Associativity relations for an additive magma.

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

        Associativity relations for a magma.

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

          Additive semigroup quotient of an additive magma.

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

          Semigroup quotient of a magma.

          Equations
          theorem AddMagma.FreeAddSemigroup.quot_mk_assoc {α : Type u} [inst : 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} [inst : 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} [inst : 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} [inst : Mul α] (x : α) (y : α) (z : α) (w : α) :
          Quot.mk (Magma.AssocRel α) (x * (y * z * w)) = Quot.mk (Magma.AssocRel α) (x * (y * (z * w)))
          def AddMagma.FreeAddSemigroup.instAddSemigroupAssocQuotient.proof_2 {α : Type u_1} [inst : 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
          Equations
          • One or more equations did not get rendered due to their size.
          Equations
          • (_ : x + y + z = x + (y + z)) = (_ : x + y + z = x + (y + z))
          Equations
          def AddMagma.FreeAddSemigroup.instAddSemigroupAssocQuotient.proof_1 {α : Type u_1} [inst : 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
          • One or more equations did not get rendered due to their size.
          Equations
          def AddMagma.FreeAddSemigroup.of.proof_1 {α : Type u_1} [inst : Add α] (_x : α) (_y : α) :
          Equations

          Embedding from additive magma to its free additive semigroup.

          Equations

          Embedding from magma to its free semigroup.

          Equations
          Equations
          • AddMagma.FreeAddSemigroup.instInhabitedAssocQuotient = { default := AddMagma.FreeAddSemigroup.of default }
          Equations
          • Magma.AssocQuotient.instInhabitedAssocQuotient = { default := Magma.AssocQuotient.of default }
          theorem AddMagma.FreeAddSemigroup.induction_on {α : Type u} [inst : Add α] {C : AddMagma.FreeAddSemigroup αProp} (x : AddMagma.FreeAddSemigroup α) (ih : (x : α) → C (AddMagma.FreeAddSemigroup.of x)) :
          C x
          theorem Magma.AssocQuotient.induction_on {α : Type u} [inst : Mul α] {C : Magma.AssocQuotient αProp} (x : Magma.AssocQuotient α) (ih : (x : α) → C (Magma.AssocQuotient.of x)) :
          C x
          theorem AddMagma.FreeAddSemigroup.hom_ext {α : Type u} [inst : Add α] {β : Type v} [inst : AddSemigroup β] {f : AddHom (AddMagma.FreeAddSemigroup α) β} {g : AddHom (AddMagma.FreeAddSemigroup α) β} (h : AddHom.comp f AddMagma.FreeAddSemigroup.of = AddHom.comp g AddMagma.FreeAddSemigroup.of) :
          f = g
          theorem Magma.AssocQuotient.hom_ext {α : Type u} [inst : Mul α] {β : Type v} [inst : Semigroup β] {f : Magma.AssocQuotient α →ₙ* β} {g : Magma.AssocQuotient α →ₙ* β} (h : MulHom.comp f Magma.AssocQuotient.of = MulHom.comp g Magma.AssocQuotient.of) :
          f = g
          def AddMagma.FreeAddSemigroup.lift.proof_2 {α : Type u_1} [inst : Add α] {β : Type u_2} [inst : AddSemigroup β] (f : AddHom α β) (x : AddMagma.FreeAddSemigroup α) (y : AddMagma.FreeAddSemigroup α) :
          (fun x => Quot.liftOn x f (_ : ∀ (a b : α), AddMagma.AssocRel α a bf a = f b)) (x + y) = (fun x => Quot.liftOn x f (_ : ∀ (a b : α), AddMagma.AssocRel α a bf a = f b)) x + (fun x => Quot.liftOn x f (_ : ∀ (a b : α), AddMagma.AssocRel α a bf a = f b)) y
          Equations
          • One or more equations did not get rendered due to their size.
          def AddMagma.FreeAddSemigroup.lift.proof_4 {α : Type u_1} [inst : Add α] {β : Type u_2} [inst : AddSemigroup β] (f : AddHom (AddMagma.FreeAddSemigroup α) β) :
          (fun f => { toFun := fun x => Quot.liftOn x f (_ : ∀ (a b : α), AddMagma.AssocRel α a bf a = f b), map_add' := (_ : ∀ (x y : AddMagma.FreeAddSemigroup α), (fun x => Quot.liftOn x f (_ : ∀ (a b : α), AddMagma.AssocRel α a bf a = f b)) (x + y) = (fun x => Quot.liftOn x f (_ : ∀ (a b : α), AddMagma.AssocRel α a bf a = f b)) x + (fun x => Quot.liftOn x f (_ : ∀ (a b : α), AddMagma.AssocRel α a bf a = f b)) y) }) ((fun f => AddHom.comp f AddMagma.FreeAddSemigroup.of) f) = f
          Equations
          • One or more equations did not get rendered due to their size.
          def AddMagma.FreeAddSemigroup.lift.proof_1 {α : Type u_1} [inst : Add α] {β : Type u_2} [inst : AddSemigroup β] (f : AddHom α β) (a : α) (b : α) :
          AddMagma.AssocRel α a bf a = f b
          Equations
          • (_ : f a = f b) = (_ : f a = f b)
          def AddMagma.FreeAddSemigroup.lift.proof_3 {α : Type u_1} [inst : Add α] {β : Type u_2} [inst : AddSemigroup β] (f : AddHom α β) :
          (fun f => AddHom.comp f AddMagma.FreeAddSemigroup.of) ((fun f => { toFun := fun x => Quot.liftOn x f (_ : ∀ (a b : α), AddMagma.AssocRel α a bf a = f b), map_add' := (_ : ∀ (x y : AddMagma.FreeAddSemigroup α), (fun x => Quot.liftOn x f (_ : ∀ (a b : α), AddMagma.AssocRel α a bf a = f b)) (x + y) = (fun x => Quot.liftOn x f (_ : ∀ (a b : α), AddMagma.AssocRel α a bf a = f b)) x + (fun x => Quot.liftOn x f (_ : ∀ (a b : α), AddMagma.AssocRel α a bf a = f b)) y) }) f) = f
          Equations
          • One or more equations did not get rendered due to their size.
          def AddMagma.FreeAddSemigroup.lift {α : Type u} [inst : Add α] {β : Type v} [inst : AddSemigroup β] :

          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.
          @[simp]
          theorem AddMagma.FreeAddSemigroup.lift_symm_apply {α : Type u} [inst : Add α] {β : Type v} [inst : AddSemigroup β] (f : AddHom (AddMagma.FreeAddSemigroup α) β) :
          ↑(Equiv.symm AddMagma.FreeAddSemigroup.lift) f = AddHom.comp f AddMagma.FreeAddSemigroup.of
          @[simp]
          theorem Magma.AssocQuotient.lift_symm_apply {α : Type u} [inst : Mul α] {β : Type v} [inst : Semigroup β] (f : Magma.AssocQuotient α →ₙ* β) :
          ↑(Equiv.symm Magma.AssocQuotient.lift) f = MulHom.comp f Magma.AssocQuotient.of
          def Magma.AssocQuotient.lift {α : Type u} [inst : Mul α] {β : Type v} [inst : 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.
          @[simp]
          theorem AddMagma.FreeAddSemigroup.lift_of {α : Type u} [inst : Add α] {β : Type v} [inst : AddSemigroup β] (f : AddHom α β) (x : α) :
          ↑(AddMagma.FreeAddSemigroup.lift f) (AddMagma.FreeAddSemigroup.of x) = f x
          @[simp]
          theorem Magma.AssocQuotient.lift_of {α : Type u} [inst : Mul α] {β : Type v} [inst : Semigroup β] (f : α →ₙ* β) (x : α) :
          ↑(Magma.AssocQuotient.lift f) (Magma.AssocQuotient.of x) = f x
          @[simp]
          theorem AddMagma.FreeAddSemigroup.lift_comp_of {α : Type u} [inst : Add α] {β : Type v} [inst : AddSemigroup β] (f : AddHom α β) :
          AddHom.comp (AddMagma.FreeAddSemigroup.lift f) AddMagma.FreeAddSemigroup.of = f
          @[simp]
          theorem Magma.AssocQuotient.lift_comp_of {α : Type u} [inst : Mul α] {β : Type v} [inst : Semigroup β] (f : α →ₙ* β) :
          MulHom.comp (Magma.AssocQuotient.lift f) Magma.AssocQuotient.of = f
          @[simp]
          theorem AddMagma.FreeAddSemigroup.lift_comp_of' {α : Type u} [inst : Add α] {β : Type v} [inst : AddSemigroup β] (f : AddHom (AddMagma.FreeAddSemigroup α) β) :
          AddMagma.FreeAddSemigroup.lift (AddHom.comp f AddMagma.FreeAddSemigroup.of) = f
          @[simp]
          theorem Magma.AssocQuotient.lift_comp_of' {α : Type u} [inst : Mul α] {β : Type v} [inst : Semigroup β] (f : Magma.AssocQuotient α →ₙ* β) :
          Magma.AssocQuotient.lift (MulHom.comp f Magma.AssocQuotient.of) = f
          def AddMagma.FreeAddSemigroup.map {α : Type u} [inst : Add α] {β : Type v} [inst : Add β] (f : AddHom α β) :

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

          Equations
          def Magma.AssocQuotient.map {α : Type u} [inst : Mul α] {β : Type v} [inst : Mul β] (f : α →ₙ* β) :

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

          Equations
          @[simp]
          theorem AddMagma.FreeAddSemigroup.map_of {α : Type u} [inst : Add α] {β : Type v} [inst : 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} [inst : Mul α] {β : Type v} [inst : Mul β] (f : α →ₙ* β) (x : α) :
          ↑(Magma.AssocQuotient.map f) (Magma.AssocQuotient.of x) = Magma.AssocQuotient.of (f x)
          structure FreeAddSemigroup (α : Type u) :
          • The head of the element

            head : α
          • The tail of the element

            tail : List α

          Free additive semigroup over a given alphabet.

          Instances For
            theorem FreeAddSemigroup.ext_iff {α : Type u} (x : FreeAddSemigroup α) (y : FreeAddSemigroup α) :
            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 FreeSemigroup.ext {α : Type u} (x : FreeSemigroup α) (y : FreeSemigroup α) (head : x.head = y.head) (tail : x.tail = y.tail) :
            x = y
            theorem FreeSemigroup.ext_iff {α : Type u} (x : FreeSemigroup α) (y : FreeSemigroup α) :
            x = y x.head = y.head x.tail = y.tail
            structure FreeSemigroup (α : Type u) :
            • The head of the element

              head : α
            • The tail of the element

              tail : List α

            Free semigroup over a given alphabet.

            Instances For
              def FreeAddSemigroup.instAddSemigroupFreeAddSemigroup.proof_1 {α : Type u_1} (_L1 : FreeAddSemigroup α) (_L2 : FreeAddSemigroup α) (_L3 : FreeAddSemigroup α) :
              _L1 + _L2 + _L3 = _L1 + (_L2 + _L3)
              Equations
              • (_ : _L1 + _L2 + _L3 = _L1 + (_L2 + _L3)) = (_ : _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 α → free_add_semigroup α→ free_add_semigroup α.

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

              The embedding α → FreeSemigroup α→ FreeSemigroup α.

              Equations

              Length of an element of free additive semigroup

              Equations

              Length of an element of free semigroup.

              Equations
              Equations
              Equations
              noncomputable 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.
              noncomputable 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.
              theorem FreeAddSemigroup.hom_ext {α : Type u} {β : Type v} [inst : Add β] {f : AddHom (FreeAddSemigroup α) β} {g : AddHom (FreeAddSemigroup α) β} (h : f FreeAddSemigroup.of = g FreeAddSemigroup.of) :
              f = g
              theorem FreeSemigroup.hom_ext {α : Type u} {β : Type v} [inst : Mul β] {f : FreeSemigroup α →ₙ* β} {g : FreeSemigroup α →ₙ* β} (h : f FreeSemigroup.of = g FreeSemigroup.of) :
              f = g
              def FreeAddSemigroup.lift {α : Type u} {β : Type v} [inst : 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.
              def FreeAddSemigroup.lift.proof_1 {α : Type u_1} {β : Type u_2} [inst : 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
              Equations
              • One or more equations did not get rendered due to their size.
              def FreeAddSemigroup.lift.proof_3 {α : Type u_1} {β : Type u_2} [inst : AddSemigroup β] (f : AddHom (FreeAddSemigroup α) β) :
              (fun f => { toFun := fun x => List.foldl (fun a b => a + f b) (f x.head) x.tail, map_add' := (_ : ∀ (x 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) }) ((fun f => f FreeAddSemigroup.of) f) = f
              Equations
              • One or more equations did not get rendered due to their size.
              def FreeAddSemigroup.lift.proof_2 {α : Type u_1} {β : Type u_2} [inst : AddSemigroup β] (f : αβ) :
              (fun f => f FreeAddSemigroup.of) ((fun f => { toFun := fun x => List.foldl (fun a b => a + f b) (f x.head) x.tail, map_add' := (_ : ∀ (x 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) }) f) = (fun f => f FreeAddSemigroup.of) ((fun f => { toFun := fun x => List.foldl (fun a b => a + f b) (f x.head) x.tail, map_add' := (_ : ∀ (x 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) }) f)
              Equations
              • One or more equations did not get rendered due to their size.
              @[simp]
              theorem FreeSemigroup.lift_symm_apply {α : Type u} {β : Type v} [inst : Semigroup β] (f : FreeSemigroup α →ₙ* β) :
              ∀ (a : α), ↑(Equiv.symm FreeSemigroup.lift) f a = (f FreeSemigroup.of) a
              @[simp]
              theorem FreeAddSemigroup.lift_symm_apply {α : Type u} {β : Type v} [inst : AddSemigroup β] (f : AddHom (FreeAddSemigroup α) β) :
              ∀ (a : α), ↑(Equiv.symm FreeAddSemigroup.lift) f a = (f FreeAddSemigroup.of) a
              def FreeSemigroup.lift {α : Type u} {β : Type v} [inst : 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.
              @[simp]
              theorem FreeAddSemigroup.lift_of {α : Type u} {β : Type v} [inst : AddSemigroup β] (f : αβ) (x : α) :
              ↑(FreeAddSemigroup.lift f) (FreeAddSemigroup.of x) = f x
              @[simp]
              theorem FreeSemigroup.lift_of {α : Type u} {β : Type v} [inst : Semigroup β] (f : αβ) (x : α) :
              ↑(FreeSemigroup.lift f) (FreeSemigroup.of x) = f x
              @[simp]
              theorem FreeAddSemigroup.lift_comp_of {α : Type u} {β : Type v} [inst : AddSemigroup β] (f : αβ) :
              ↑(FreeAddSemigroup.lift f) FreeAddSemigroup.of = f
              @[simp]
              theorem FreeSemigroup.lift_comp_of {α : Type u} {β : Type v} [inst : Semigroup β] (f : αβ) :
              ↑(FreeSemigroup.lift f) FreeSemigroup.of = f
              @[simp]
              theorem FreeAddSemigroup.lift_comp_of' {α : Type u} {β : Type v} [inst : AddSemigroup β] (f : AddHom (FreeAddSemigroup α) β) :
              FreeAddSemigroup.lift (f FreeAddSemigroup.of) = f
              @[simp]
              theorem FreeSemigroup.lift_comp_of' {α : Type u} {β : Type v} [inst : Semigroup β] (f : FreeSemigroup α →ₙ* β) :
              FreeSemigroup.lift (f FreeSemigroup.of) = f
              theorem FreeAddSemigroup.lift_of_add {α : Type u} {β : Type v} [inst : 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} [inst : 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
              def FreeSemigroup.map {α : Type u} {β : Type v} (f : αβ) :

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

              Equations
              @[simp]
              theorem FreeAddSemigroup.map_of {α : Type u} {β : Type v} (f : αβ) (x : α) :
              @[simp]
              theorem FreeSemigroup.map_of {α : Type u} {β : Type v} (f : αβ) (x : α) :
              @[simp]
              theorem FreeSemigroup.length_map {α : Type u} {β : Type v} (f : αβ) (x : FreeSemigroup α) :
              noncomputable 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
              noncomputable 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
              @[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 => x) = f <$> x
              @[simp]
              theorem FreeSemigroup.pure_seq {α : Type u} {β : Type u} {f : αβ} {x : FreeSemigroup α} :
              (Seq.seq (pure f) fun x => x) = f <$> x
              @[simp]
              theorem FreeAddSemigroup.add_seq {α : Type u} {β : Type u} {f : FreeAddSemigroup (αβ)} {g : FreeAddSemigroup (αβ)} {x : FreeAddSemigroup α} :
              (Seq.seq (f + g) fun x => x) = (Seq.seq f fun x => x) + Seq.seq g fun x => x
              @[simp]
              theorem FreeSemigroup.mul_seq {α : Type u} {β : Type u} {f : FreeSemigroup (αβ)} {g : FreeSemigroup (αβ)} {x : FreeSemigroup α} :
              (Seq.seq (f * g) fun x => x) = (Seq.seq f fun x => x) * Seq.seq g fun x => x
              noncomputable def FreeAddSemigroup.traverse {m : Type u → Type u} [inst : Applicative m] {α : Type u} {β : Type u} (F : αm β) (x : FreeAddSemigroup α) :

              FreeAddSemigroup is traversable.

              Equations
              noncomputable def FreeSemigroup.traverse {m : Type u → Type u} [inst : Applicative m] {α : Type u} {β : Type u} (F : αm β) (x : FreeSemigroup α) :

              FreeSemigroup is traversable.

              Equations
              @[simp]
              theorem FreeAddSemigroup.traverse_pure {α : Type u} {β : Type u} {m : Type u → Type u} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : Applicative m] (F : αm β) [inst : LawfulApplicative m] (x : FreeAddSemigroup α) (y : FreeAddSemigroup α) :
              traverse F (x + y) = Seq.seq ((fun x x_1 => x + x_1) <$> traverse F x) fun x => traverse F y
              @[simp]
              theorem FreeSemigroup.traverse_mul {α : Type u} {β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : αm β) [inst : LawfulApplicative m] (x : FreeSemigroup α) (y : FreeSemigroup α) :
              traverse F (x * y) = Seq.seq ((fun x x_1 => x * x_1) <$> traverse F x) fun x => traverse F y
              @[simp]
              theorem FreeAddSemigroup.traverse_add' {α : Type u} {β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : αm β) [inst : LawfulApplicative m] :
              Function.comp (traverse F) Add.add = fun x y => Seq.seq ((fun x x_1 => x + x_1) <$> traverse F x) fun x => traverse F y
              @[simp]
              theorem FreeSemigroup.traverse_mul' {α : Type u} {β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : αm β) [inst : LawfulApplicative m] :
              Function.comp (traverse F) Mul.mul = fun x y => Seq.seq ((fun x x_1 => x * x_1) <$> traverse F x) fun x => traverse F y
              @[simp]
              theorem FreeAddSemigroup.traverse_eq {α : Type u} {β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : αm β) (x : FreeAddSemigroup α) :
              @[simp]
              theorem FreeSemigroup.traverse_eq {α : Type u} {β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : αm β) (x : FreeSemigroup α) :
              @[simp]
              theorem FreeAddSemigroup.add_map_seq {α : Type u} (x : FreeAddSemigroup α) (y : FreeAddSemigroup α) :
              (Seq.seq ((fun x x_1 => x + x_1) <$> x) fun x => y) = x + y
              @[simp]
              theorem FreeSemigroup.mul_map_seq {α : Type u} (x : FreeSemigroup α) (y : FreeSemigroup α) :
              (Seq.seq ((fun x x_1 => x * x_1) <$> x) fun x => y) = x * y
              Equations
              • One or more equations did not get rendered due to their size.
              def FreeAddSemigroup.instIsLawfulTraversableFreeAddSemigroupInstTraversableFreeAddSemigroup.proof_3 :
              ∀ {F G : Type u_1 → Type u_1} [inst : Applicative F] [inst_1 : Applicative G] [inst_2 : LawfulApplicative F] [inst_3 : LawfulApplicative G] {α β γ : Type u_1} (f : βF γ) (g : αG β) (x : FreeAddSemigroup α), traverse (Functor.Comp.mk Functor.map f g) x = Functor.Comp.mk (traverse f <$> traverse g x)
              Equations
              • One or more equations did not get rendered due to their size.
              def FreeAddSemigroup.instIsLawfulTraversableFreeAddSemigroupInstTraversableFreeAddSemigroup.proof_5 :
              ∀ {F G : Type u_1 → Type u_1} [inst : Applicative F] [inst_1 : Applicative G] [inst_2 : LawfulApplicative F] [inst_3 : LawfulApplicative G] (η : ApplicativeTransformation F G) (α β : Type u_1) (f : αF β) (x : FreeAddSemigroup α), (fun {α} => ApplicativeTransformation.app η α) (traverse f x) = traverse ((fun {α} => ApplicativeTransformation.app η α) f) x
              Equations
              • One or more equations did not get rendered due to their size.
              Equations
              Equations
              • One or more equations did not get rendered due to their size.
              Equations
              Equations

              The canonical additive morphism from FreeAddMagma α to FreeAddSemigroup α.

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

              The canonical multiplicative morphism from FreeMagma α to FreeSemigroup α.

              Equations
              • FreeMagma.toFreeSemigroup = FreeMagma.lift FreeSemigroup.of
              @[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 : αβ) :
              AddHom.comp FreeAddMagma.toFreeAddSemigroup (FreeAddMagma.map f) = AddHom.comp (FreeAddSemigroup.map f) FreeAddMagma.toFreeAddSemigroup
              theorem FreeMagma.toFreeSemigroup_comp_map {α : Type u} {β : Type v} (f : αβ) :
              MulHom.comp FreeMagma.toFreeSemigroup (FreeMagma.map f) = MulHom.comp (FreeSemigroup.map f) 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 α) :
              FreeAddSemigroup.length (FreeAddMagma.toFreeAddSemigroup x) = FreeAddMagma.length x
              @[simp]
              theorem FreeMagma.length_toFreeSemigroup {α : Type u} (x : FreeMagma α) :
              FreeSemigroup.length (FreeMagma.toFreeSemigroup x) = FreeMagma.length x
              def FreeAddMagmaAssocQuotientEquiv.proof_1 (α : Type u_1) :
              AddHom.comp (FreeAddSemigroup.lift (AddMagma.FreeAddSemigroup.of FreeAddMagma.of)) (AddMagma.FreeAddSemigroup.lift FreeAddMagma.toFreeAddSemigroup) = AddHom.id (AddMagma.FreeAddSemigroup (FreeAddMagma α))
              Equations
              • One or more equations did not get rendered due to their size.
              def FreeAddMagmaAssocQuotientEquiv.proof_2 (α : Type u_1) :
              AddHom.comp (AddMagma.FreeAddSemigroup.lift FreeAddMagma.toFreeAddSemigroup) (FreeAddSemigroup.lift (AddMagma.FreeAddSemigroup.of FreeAddMagma.of)) = AddHom.id (FreeAddSemigroup α)
              Equations
              • One or more equations did not get rendered due to their size.

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

              Equations
              • One or more equations did not get rendered due to their size.

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

              Equations
              • One or more equations did not get rendered due to their size.