algebra.free

# Free constructions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

## Main definitions #

• `free_magma α`: free magma (structure with binary operation without any axioms) over alphabet `α`, defined inductively, with traversable instance and decidable equality.
• `magma.assoc_quotient α`: quotient of a magma `α` by the associativity equivalence relation.
• `free_semigroup α`: free semigroup over alphabet `α`, defined as a structure with two fields `head : α` and `tail : list α` (i.e. nonempty lists), with traversable instance and decidable equality.
• `free_magma_assoc_quotient_equiv α`: isomorphism between `magma.assoc_quotient (free_magma α)` and `free_semigroup α`.
• `free_magma.lift`: the universal property of the free magma, expressing its adjointness.
inductive free_magma (α : Type u) :

Free magma over a given alphabet.

Instances for `free_magma`
@[protected, instance]
def free_magma.decidable_eq (α : Type u) [a : decidable_eq α] :
@[protected, instance]
def free_add_magma.decidable_eq (α : Type u) [a : decidable_eq α] :
inductive free_add_magma (α : Type u) :

Free nonabelian additive magma over a given alphabet.

Instances for `free_add_magma`
@[protected, instance]
def free_add_magma.inhabited {α : Type u} [inhabited α] :
Equations
@[protected, instance]
def free_magma.inhabited {α : Type u} [inhabited α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
def free_magma.has_mul {α : Type u} :
Equations
@[simp]
theorem free_magma.mul_eq {α : Type u} (x y : free_magma α) :
x.mul y = x * y
@[simp]
x.add y = x + y
def free_add_magma.rec_on_add {α : Type u} {C : Sort l} (x : free_add_magma α) (ih1 : Π (x : α), C ) (ih2 : Π (x y : , C x C y C (x + y)) :
C x

Recursor for `free_add_magma` using `x + y` instead of `free_add_magma.add x y`.

Equations
def free_magma.rec_on_mul {α : Type u} {C : Sort l} (x : free_magma α) (ih1 : Π (x : α), C ) (ih2 : Π (x y : , C x C y C (x * y)) :
C x

Recursor for `free_magma` using `x * y` instead of `free_magma.mul x y`.

Equations
@[ext]
theorem free_add_magma.hom_ext {α : Type u} {β : Type v} [has_add β] {f g : β} (h : = ) :
f = g
@[ext]
theorem free_magma.hom_ext {α : Type u} {β : Type v} [has_mul β] {f g : →ₙ* β} (h : = ) :
f = g
def free_magma.lift_aux {α : Type u} {β : Type v} [has_mul β] (f : α β) :
β

Lifts a function `α → β` to a magma homomorphism `free_magma α → β` given a magma `β`.

Equations
• (x * y) =
• = f x
def free_add_magma.lift_aux {α : Type u} {β : Type v} [has_add β] (f : α β) :

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

Equations
• (x + y) =
@[simp]
theorem free_add_magma.lift_symm_apply {α : Type u} {β : Type v} [has_add β] (F : β) (ᾰ : α) :
=
@[simp]
theorem free_magma.lift_symm_apply {α : Type u} {β : Type v} [has_mul β] (F : →ₙ* β) (ᾰ : α) :
def free_add_magma.lift {α : Type u} {β : Type v} [has_add β] :
β) β

Equations
def free_magma.lift {α : Type u} {β : Type v} [has_mul β] :
β) →ₙ* β)

The universal property of the free magma expressing its adjointness.

Equations
@[simp]
theorem free_add_magma.lift_of {α : Type u} {β : Type v} [has_add β] (f : α β) (x : α) :
= f x
@[simp]
theorem free_magma.lift_of {α : Type u} {β : Type v} [has_mul β] (f : α β) (x : α) :
= f x
@[simp]
theorem free_magma.lift_comp_of {α : Type u} {β : Type v} [has_mul β] (f : α β) :
@[simp]
theorem free_add_magma.lift_comp_of {α : Type u} {β : Type v} [has_add β] (f : α β) :
@[simp]
theorem free_add_magma.lift_comp_of' {α : Type u} {β : Type v} [has_add β] (f : β) :
@[simp]
theorem free_magma.lift_comp_of' {α : Type u} {β : Type v} [has_mul β] (f : →ₙ* β) :
def free_add_magma.map {α : Type u} {β : Type v} (f : α β) :

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

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

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

Equations
@[simp]
theorem free_add_magma.map_of {α : Type u} {β : Type v} (f : α β) (x : α) :
@[simp]
theorem free_magma.map_of {α : Type u} {β : Type v} (f : α β) (x : α) :
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected]
def free_add_magma.rec_on_pure {α : Type u} {C : Sort l} (x : free_add_magma α) (ih1 : Π (x : α), C ) (ih2 : Π (x y : , C x C y C (x + y)) :
C x

Recursor on `free_add_magma` using `pure` instead of `of`.

Equations
@[protected]
def free_magma.rec_on_pure {α : Type u} {C : Sort l} (x : free_magma α) (ih1 : Π (x : α), C ) (ih2 : Π (x y : , C x C y C (x * y)) :
C x

Recursor on `free_magma` using `pure` instead of `of`.

Equations
@[simp]
theorem free_magma.map_pure {α β : Type u} (f : α β) (x : α) :
@[simp]
theorem free_add_magma.map_pure {α β : Type u} (f : α β) (x : α) :
@[simp]
theorem free_magma.map_mul' {α β : Type u} (f : α β) (x y : free_magma α) :
f <\$> (x * y) = f <\$> x * f <\$> y
@[simp]
theorem free_add_magma.map_add' {α β : Type u} (f : α β) (x y : free_add_magma α) :
f <\$> (x + y) = f <\$> x + f <\$> y
@[simp]
theorem free_add_magma.pure_bind {α β : Type u} (f : α ) (x : α) :
= f x
@[simp]
theorem free_magma.pure_bind {α β : Type u} (f : α ) (x : α) :
= f x
@[simp]
theorem free_add_magma.add_bind {α β : Type u} (f : α ) (x y : free_add_magma α) :
x + y >>= f = (x >>= f) + (y >>= f)
@[simp]
theorem free_magma.mul_bind {α β : Type u} (f : α ) (x y : free_magma α) :
x * y >>= f = (x >>= f) * (y >>= f)
@[simp]
theorem free_add_magma.pure_seq {α β : Type u} {f : α β} {x : free_add_magma α} :
= f <\$> x
@[simp]
theorem free_magma.pure_seq {α β : Type u} {f : α β} {x : free_magma α} :
= f <\$> x
@[simp]
f + g <*> x = (f <*> x) + (g <*> x)
@[simp]
theorem free_magma.mul_seq {α β : Type u} {f g : free_magma β)} {x : free_magma α} :
f * g <*> x = (f <*> x) * (g <*> x)
@[protected, instance]
@[protected, instance]
@[protected]
def free_magma.traverse {m : Type u Type u} [applicative m] {α β : Type u} (F : α m β) :
m (free_magma β)

`free_magma` is traversable.

Equations
• (x * y) =
@[protected]
def free_add_magma.traverse {m : Type u Type u} [applicative m] {α β : Type u} (F : α m β) :
m

`free_add_magma` is traversable.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem free_magma.traverse_pure {α β : Type u} {m : Type u Type u} [applicative m] (F : α m β) (x : α) :
@[simp]
theorem free_add_magma.traverse_pure {α β : Type u} {m : Type u Type u} [applicative m] (F : α m β) (x : α) :
@[simp]
theorem free_add_magma.traverse_pure' {α β : Type u} {m : Type u Type u} [applicative m] (F : α m β) :
= λ (x : α),
@[simp]
theorem free_magma.traverse_pure' {α β : Type u} {m : Type u Type u} [applicative m] (F : α m β) :
= λ (x : α),
@[simp]
theorem free_add_magma.traverse_add {α β : Type u} {m : Type u Type u} [applicative m] (F : α m β) (x y : free_add_magma α) :
(x + y) =
@[simp]
theorem free_magma.traverse_mul {α β : Type u} {m : Type u Type u} [applicative m] (F : α m β) (x y : free_magma α) :
(x * y) =
@[simp]
theorem free_magma.traverse_mul' {α β : Type u} {m : Type u Type u} [applicative m] (F : α m β) :
= λ (x y : ,
@[simp]
theorem free_add_magma.traverse_add' {α β : Type u} {m : Type u Type u} [applicative m] (F : α m β) :
= λ (x y : ,
@[simp]
theorem free_magma.traverse_eq {α β : Type u} {m : Type u Type u} [applicative m] (F : α m β) (x : free_magma α) :
@[simp]
theorem free_add_magma.traverse_eq {α β : Type u} {m : Type u Type u} [applicative m] (F : α m β) (x : free_add_magma α) :
@[simp]
= x + y
@[simp]
theorem free_magma.mul_map_seq {α : Type u} (x y : free_magma α) :
= x * y
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected]
def free_magma.repr {α : Type u} [has_repr α] :

Representation of an element of a free magma.

Equations
@[protected]
def free_add_magma.repr {α : Type u} [has_repr α] :

Representation of an element of a free additive magma.

Equations
@[protected, instance]
def free_magma.has_repr {α : Type u} [has_repr α] :
Equations
@[protected, instance]
def free_add_magma.has_repr {α : Type u} [has_repr α] :
Equations
@[simp]
def free_magma.length {α : Type u} :

Length of an element of a free magma.

Equations
@[simp]
def free_add_magma.length {α : Type u} :

Length of an element of a free additive magma.

Equations
α α Prop
• intro : {α : Type u} [_inst_1 : has_add α] (x y z : α), (x + y + z) (x + (y + z))
• left : {α : Type u} [_inst_1 : has_add α] (w x y z : α), (w + (x + y + z)) (w + (x + (y + z)))

Associativity relations for an additive magma.

inductive magma.assoc_rel (α : Type u) [has_mul α] :
α α Prop
• intro : {α : Type u} [_inst_1 : has_mul α] (x y z : α), (x * y * z) (x * (y * z))
• left : {α : Type u} [_inst_1 : has_mul α] (w x y z : α), (w * (x * y * z)) (w * (x * (y * z)))

Associativity relations for a magma.

def magma.assoc_quotient (α : Type u) [has_mul α] :

Semigroup quotient of a magma.

Equations
• = quot
Instances for `magma.assoc_quotient`

Equations
Instances for `add_magma.free_add_semigroup`
quot.mk (x + y + z) = quot.mk (x + (y + z))
theorem magma.assoc_quotient.quot_mk_assoc {α : Type u} [has_mul α] (x y z : α) :
quot.mk (x * y * z) = quot.mk (x * (y * z))
theorem magma.assoc_quotient.quot_mk_assoc_left {α : Type u} [has_mul α] (x y z w : α) :
quot.mk (x * (y * z * w)) = quot.mk (x * (y * (z * w)))
quot.mk (x + (y + z + w)) = quot.mk (x + (y + (z + w)))
@[protected, instance]
Equations
@[protected, instance]
Equations
def magma.assoc_quotient.of {α : Type u} [has_mul α] :

Embedding from magma to its free semigroup.

Equations

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected]
theorem add_magma.free_add_semigroup.induction_on {α : Type u} [has_add α] {C : Prop} (ih : (x : α), ) :
C x
@[protected]
theorem magma.assoc_quotient.induction_on {α : Type u} [has_mul α] {C : Prop} (x : magma.assoc_quotient α) (ih : (x : α), ) :
C x
@[ext]
theorem magma.assoc_quotient.hom_ext {α : Type u} [has_mul α] {β : Type v} [semigroup β] {f g : →ₙ* β}  :
f = g
@[ext]
theorem add_magma.free_add_semigroup.hom_ext {α : Type u} [has_add α] {β : Type v} {f g : β}  :
f = g
β

Lifts an additive magma homomorphism `α → β` to an additive semigroup homomorphism `add_magma.assoc_quotient α → β` given an additive semigroup `β`.

Equations
@[simp]
@[simp]
theorem magma.assoc_quotient.lift_symm_apply {α : Type u} [has_mul α] {β : Type v} [semigroup β] (f : →ₙ* β) :
def magma.assoc_quotient.lift {α : Type u} [has_mul α] {β : Type v} [semigroup β] :
→ₙ* β)

Lifts a magma homomorphism `α → β` to a semigroup homomorphism `magma.assoc_quotient α → β` given a semigroup `β`.

Equations
@[simp]
theorem magma.assoc_quotient.lift_of {α : Type u} [has_mul α] {β : Type v} [semigroup β] (f : α →ₙ* β) (x : α) :
@[simp]
theorem add_magma.free_add_semigroup.lift_of {α : Type u} [has_add α] {β : Type v} (f : β) (x : α) :
@[simp]
theorem magma.assoc_quotient.lift_comp_of {α : Type u} [has_mul α] {β : Type v} [semigroup β] (f : α →ₙ* β) :
@[simp]
@[simp]
@[simp]
theorem magma.assoc_quotient.lift_comp_of' {α : Type u} [has_mul α] {β : Type v} [semigroup β] (f : →ₙ* β) :
def magma.assoc_quotient.map {α : Type u} [has_mul α] {β : Type v} [has_mul β] (f : α →ₙ* β) :

From a magma homomorphism `α →ₙ* β` to a semigroup homomorphism `magma.assoc_quotient α →ₙ* magma.assoc_quotient β`.

Equations

From an additive magma homomorphism `α → β` to an additive semigroup homomorphism `add_magma.assoc_quotient α → add_magma.assoc_quotient β`.

Equations
@[simp]
@[simp]
theorem magma.assoc_quotient.map_of {α : Type u} [has_mul α] {β : Type v} [has_mul β] (f : α →ₙ* β) (x : α) :
x = y
@[ext]
structure free_add_semigroup (α : Type u) :
• tail : list α

Free additive semigroup over a given alphabet.

Instances for `free_add_semigroup`
theorem free_add_semigroup.ext_iff {α : Type u} (x y : free_add_semigroup α) :
theorem free_semigroup.ext {α : Type u} (x y : free_semigroup α) (h : x.head = y.head) (h_1 : x.tail = y.tail) :
x = y
@[ext]
structure free_semigroup (α : Type u) :
• tail : list α

Free semigroup over a given alphabet.

Instances for `free_semigroup`
theorem free_semigroup.ext_iff {α : Type u} (x y : free_semigroup α) :
@[protected, instance]
def free_semigroup.semigroup {α : Type u} :
Equations
@[protected, instance]
Equations
@[simp]
theorem free_semigroup.head_mul {α : Type u} (x y : free_semigroup α) :
@[simp]
@[simp]
(x + y).tail = x.tail ++ y.head :: y.tail
@[simp]
theorem free_semigroup.tail_mul {α : Type u} (x y : free_semigroup α) :
(x * y).tail = x.tail ++ y.head :: y.tail
@[simp]
theorem free_add_semigroup.mk_add_mk {α : Type u} (x y : α) (L1 L2 : list α) :
{head := x, tail := L1} + {head := y, tail := L2} = {head := x, tail := L1 ++ y :: L2}
@[simp]
theorem free_semigroup.mk_mul_mk {α : Type u} (x y : α) (L1 L2 : list α) :
{head := x, tail := L1} * {head := y, tail := L2} = {head := x, tail := L1 ++ y :: L2}
def free_semigroup.of {α : Type u} (x : α) :

The embedding `α → free_semigroup α`.

Equations
@[simp]
theorem free_add_semigroup.of_tail {α : Type u} (x : α) :
@[simp]
@[simp]
theorem free_semigroup.of_head {α : Type u} (x : α) :
= x
def free_add_semigroup.of {α : Type u} (x : α) :

The embedding `α → free_add_semigroup α`.

Equations
@[simp]
theorem free_semigroup.of_tail {α : Type u} (x : α) :
def free_semigroup.length {α : Type u} (x : free_semigroup α) :

Length of an element of free semigroup.

Equations

Length of an element of free additive semigroup

Equations
@[simp]
theorem free_semigroup.length_mul {α : Type u} (x y : free_semigroup α) :
(x * y).length = x.length + y.length
@[simp]
(x + y).length = x.length + y.length
@[simp]
theorem free_semigroup.length_of {α : Type u} (x : α) :
= 1
@[simp]
theorem free_add_semigroup.length_of {α : Type u} (x : α) :
@[protected, instance]
Equations
@[protected, instance]
def free_semigroup.inhabited {α : Type u} [inhabited α] :
Equations
@[protected]
def free_add_semigroup.rec_on_add {α : Type u} {C : Sort l} (x : free_add_semigroup α) (ih1 : Π (x : α), ) (ih2 : Π (x : α) (y : , C y C ) :
C x

Recursor for free additive semigroup using `of` and `+`.

Equations
• x.rec_on_add ih1 ih2 = x.rec_on (λ (f : α) (s : list α), s.rec_on ih1 (λ (hd : α) (tl : list α) (ih : Π (_a : α), C {head := _a, tail := tl}) (f : α), ih2 f {head := hd, tail := tl} (ih1 f) (ih hd)) f)
@[protected]
def free_semigroup.rec_on_mul {α : Type u} {C : Sort l} (x : free_semigroup α) (ih1 : Π (x : α), C ) (ih2 : Π (x : α) (y : , C C y C * y)) :
C x

Recursor for free semigroup using `of` and `*`.

Equations
• x.rec_on_mul ih1 ih2 = x.rec_on (λ (f : α) (s : list α), s.rec_on ih1 (λ (hd : α) (tl : list α) (ih : Π (_a : α), C {head := _a, tail := tl}) (f : α), ih2 f {head := hd, tail := tl} (ih1 f) (ih hd)) f)
@[ext]
theorem free_semigroup.hom_ext {α : Type u} {β : Type v} [has_mul β] {f g : →ₙ* β} (h : = ) :
f = g
@[ext]
theorem free_add_semigroup.hom_ext {α : Type u} {β : Type v} [has_add β] {f g : β}  :
f = g
@[simp]
theorem free_semigroup.lift_symm_apply {α : Type u} {β : Type v} [semigroup β] (f : →ₙ* β) (ᾰ : α) :
=
@[simp]
theorem free_add_semigroup.lift_symm_apply {α : Type u} {β : Type v} (f : β) (ᾰ : α) :
=
def free_semigroup.lift {α : Type u} {β : Type v} [semigroup β] :
β) →ₙ* β)

Lifts a function `α → β` to a semigroup homomorphism `free_semigroup α → β` given a semigroup `β`.

Equations
def free_add_semigroup.lift {α : Type u} {β : Type v}  :
β)

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

Equations
@[simp]
theorem free_semigroup.lift_of {α : Type u} {β : Type v} [semigroup β] (f : α β) (x : α) :
= f x
@[simp]
theorem free_add_semigroup.lift_of {α : Type u} {β : Type v} (f : α β) (x : α) :
= f x
@[simp]
theorem free_add_semigroup.lift_comp_of {α : Type u} {β : Type v} (f : α β) :
@[simp]
theorem free_semigroup.lift_comp_of {α : Type u} {β : Type v} [semigroup β] (f : α β) :
@[simp]
theorem free_semigroup.lift_comp_of' {α : Type u} {β : Type v} [semigroup β] (f : →ₙ* β) :
@[simp]
theorem free_add_semigroup.lift_comp_of' {α : Type u} {β : Type v} (f : β) :
theorem free_add_semigroup.lift_of_add {α : Type u} {β : Type v} (f : α β) (x : α) (y : free_add_semigroup α) :
= f x +
theorem free_semigroup.lift_of_mul {α : Type u} {β : Type v} [semigroup β] (f : α β) (x : α) (y : free_semigroup α) :
* y) = f x *
def free_semigroup.map {α : Type u} {β : Type v} (f : α β) :

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

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

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

Equations
@[simp]
theorem free_add_semigroup.map_of {α : Type u} {β : Type v} (f : α β) (x : α) :
@[simp]
theorem free_semigroup.map_of {α : Type u} {β : Type v} (f : α β) (x : α) :
@[simp]
theorem free_semigroup.length_map {α : Type u} {β : Type v} (f : α β) (x : free_semigroup α) :
@[simp]
theorem free_add_semigroup.length_map {α : Type u} {β : Type v} (f : α β) (x : free_add_semigroup α) :
@[protected, instance]
Equations
@[protected, instance]
Equations
def free_semigroup.rec_on_pure {α : Type u} {C : Sort l} (x : free_semigroup α) (ih1 : Π (x : α), C ) (ih2 : Π (x : α) (y : , C C y C * y)) :
C x

Recursor that uses `pure` instead of `of`.

Equations
def free_add_semigroup.rec_on_pure {α : Type u} {C : Sort l} (x : free_add_semigroup α) (ih1 : Π (x : α), C ) (ih2 : Π (x : α) (y : , C C y C + y)) :
C x

Recursor that uses `pure` instead of `of`.

Equations
@[simp]
theorem free_semigroup.map_pure {α β : Type u} (f : α β) (x : α) :
@[simp]
theorem free_add_semigroup.map_pure {α β : Type u} (f : α β) (x : α) :
@[simp]
theorem free_add_semigroup.map_add' {α β : Type u} (f : α β) (x y : free_add_semigroup α) :
f <\$> (x + y) = f <\$> x + f <\$> y
@[simp]
theorem free_semigroup.map_mul' {α β : Type u} (f : α β) (x y : free_semigroup α) :
f <\$> (x * y) = f <\$> x * f <\$> y
@[simp]
theorem free_add_semigroup.pure_bind {α β : Type u} (f : α ) (x : α) :
= f x
@[simp]
theorem free_semigroup.pure_bind {α β : Type u} (f : α ) (x : α) :
= f x
@[simp]
theorem free_add_semigroup.add_bind {α β : Type u} (f : α ) (x y : free_add_semigroup α) :
x + y >>= f = (x >>= f) + (y >>= f)
@[simp]
theorem free_semigroup.mul_bind {α β : Type u} (f : α ) (x y : free_semigroup α) :
x * y >>= f = (x >>= f) * (y >>= f)
@[simp]
theorem free_add_semigroup.pure_seq {α β : Type u} {f : α β} {x : free_add_semigroup α} :
= f <\$> x
@[simp]
theorem free_semigroup.pure_seq {α β : Type u} {f : α β} {x : free_semigroup α} :
= f <\$> x
@[simp]
theorem free_semigroup.mul_seq {α β : Type u} {f g : free_semigroup β)} {x : free_semigroup α} :
f * g <*> x = (f <*> x) * (g <*> x)
@[simp]
f + g <*> x = (f <*> x) + (g <*> x)
@[protected, instance]
@[protected, instance]
@[protected]
def free_add_semigroup.traverse {m : Type u Type u} [applicative m] {α β : Type u} (F : α m β) (x : free_add_semigroup α) :
m

`free_add_semigroup` is traversable.

Equations
@[protected]
def free_semigroup.traverse {m : Type u Type u} [applicative m] {α β : Type u} (F : α m β) (x : free_semigroup α) :
m

`free_semigroup` is traversable.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem free_add_semigroup.traverse_pure {α β : Type u} {m : Type u Type u} [applicative m] (F : α m β) (x : α) :
@[simp]
theorem free_semigroup.traverse_pure {α β : Type u} {m : Type u Type u} [applicative m] (F : α m β) (x : α) :
@[simp]
theorem free_add_semigroup.traverse_pure' {α β : Type u} {m : Type u Type u} [applicative m] (F : α m β) :
= λ (x : α),
@[simp]
theorem free_semigroup.traverse_pure' {α β : Type u} {m : Type u Type u} [applicative m] (F : α m β) :
= λ (x : α),
@[simp]
theorem free_add_semigroup.traverse_add {α β : Type u} {m : Type u Type u} [applicative m] (F : α m β) (x y : free_add_semigroup α) :
(x + y) =
@[simp]
theorem free_semigroup.traverse_mul {α β : Type u} {m : Type u Type u} [applicative m] (F : α m β) (x y : free_semigroup α) :
(x * y) =
@[simp]
theorem free_add_semigroup.traverse_add' {α β : Type u} {m : Type u Type u} [applicative m] (F : α m β)  :
= λ (x y : ,
@[simp]
theorem free_semigroup.traverse_mul' {α β : Type u} {m : Type u Type u} [applicative m] (F : α m β)  :
= λ (x y : ,
@[simp]
theorem free_semigroup.traverse_eq {α β : Type u} {m : Type u Type u} [applicative m] (F : α m β) (x : free_semigroup α) :
@[simp]
theorem free_add_semigroup.traverse_eq {α β : Type u} {m : Type u Type u} [applicative m] (F : α m β) (x : free_add_semigroup α) :
@[simp]
= x + y
@[simp]
theorem free_semigroup.mul_map_seq {α : Type u} (x y : free_semigroup α) :
= x * y
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations

The canonical additive morphism from `free_add_magma α` to `free_add_semigroup α`.

Equations

The canonical multiplicative morphism from `free_magma α` to `free_semigroup α`.

Equations
@[simp]
theorem free_magma.to_free_semigroup_of {α : Type u} (x : α) :
@[simp]
@[simp]
@[simp]
theorem free_magma.to_free_semigroup_comp_map {α : Type u} {β : Type v} (f : α β) :
theorem free_add_magma.to_free_add_semigroup_comp_map {α : Type u} {β : Type v} (f : α β) :
theorem free_magma.to_free_semigroup_map {α : Type u} {β : Type v} (f : α β) (x : free_magma α) :
theorem free_add_magma.to_free_add_semigroup_map {α : Type u} {β : Type v} (f : α β) (x : free_add_magma α) :
@[simp]
theorem free_magma.length_to_free_semigroup {α : Type u} (x : free_magma α) :

Isomorphism between `add_magma.assoc_quotient (free_add_magma α)` and `free_add_semigroup α`.

Equations

Isomorphism between `magma.assoc_quotient (free_magma α)` and `free_semigroup α`.

Equations