Documentation

Mathlib.Algebra.Free

Free constructions #

Main definitions #

inductive FreeAddMagma (α : Type u) :

Free nonabelian additive magma over a given alphabet.

inductive FreeMagma (α : Type u) :

Free magma over a given alphabet.

instance FreeMagma.instMul {α : Type u} :
Equations
@[simp]
theorem FreeMagma.mul_eq {α : Type u} (x y : FreeMagma α) :
x.mul y = x * y
@[simp]
theorem FreeAddMagma.add_eq {α : Type u} (x y : FreeAddMagma α) :
x.add y = x + y
def FreeMagma.recOnMul {α : Type u} {C : FreeMagma αSort l} (x : FreeMagma α) (ih1 : (x : α) → C (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
def FreeAddMagma.recOnAdd {α : Type u} {C : FreeAddMagma αSort l} (x : FreeAddMagma α) (ih1 : (x : α) → C (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
theorem FreeAddMagma.hom_ext {α : Type u} {β : Type v} [Add β] {f g : FreeAddMagma α →ₙ+ β} (h : f of = g of) :
f = g
theorem FreeMagma.hom_ext {α : Type u} {β : Type v} [Mul β] {f g : FreeMagma α →ₙ* β} (h : f of = g 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
def FreeAddMagma.liftAux {α : Type u} {β : Type v} [Add β] (f : αβ) :
FreeAddMagma αβ

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

Equations
def FreeMagma.lift {α : Type u} {β : Type v} [Mul β] :
(αβ) (FreeMagma α →ₙ* β)

The universal property of the free magma expressing its adjointness.

Equations
def FreeAddMagma.lift {α : Type u} {β : Type v} [Add β] :
(αβ) (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.
@[simp]
theorem FreeAddMagma.lift_symm_apply {α : Type u} {β : Type v} [Add β] (F : FreeAddMagma α →ₙ+ β) (a✝ : α) :
lift.symm F a✝ = (F of) a✝
@[simp]
theorem FreeMagma.lift_symm_apply {α : Type u} {β : Type v} [Mul β] (F : FreeMagma α →ₙ* β) (a✝ : α) :
lift.symm F a✝ = (F of) a✝
@[simp]
theorem FreeMagma.lift_of {α : Type u} {β : Type v} [Mul β] (f : αβ) (x : α) :
(lift f) (of x) = f x
@[simp]
theorem FreeAddMagma.lift_of {α : Type u} {β : Type v} [Add β] (f : αβ) (x : α) :
(lift f) (of x) = f x
@[simp]
theorem FreeMagma.lift_comp_of {α : Type u} {β : Type v} [Mul β] (f : αβ) :
(lift f) of = f
@[simp]
theorem FreeAddMagma.lift_comp_of {α : Type u} {β : Type v} [Add β] (f : αβ) :
(lift f) of = f
@[simp]
theorem FreeMagma.lift_comp_of' {α : Type u} {β : Type v} [Mul β] (f : FreeMagma α →ₙ* β) :
lift (f of) = f
@[simp]
theorem FreeAddMagma.lift_comp_of' {α : Type u} {β : Type v} [Add β] (f : FreeAddMagma α →ₙ+ β) :
lift (f of) = f
def FreeMagma.map {α : Type u} {β : Type v} (f : αβ) :

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

Equations
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
@[simp]
theorem FreeMagma.map_of {α : Type u} {β : Type v} (f : αβ) (x : α) :
(map f) (of x) = of (f x)
@[simp]
theorem FreeAddMagma.map_of {α : Type u} {β : Type v} (f : αβ) (x : α) :
(map f) (of x) = of (f x)
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
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
@[simp]
theorem FreeMagma.map_pure {α β : Type u} (f : αβ) (x : α) :
f <$> pure x = pure (f x)
@[simp]
theorem FreeAddMagma.map_pure {α β : Type u} (f : αβ) (x : α) :
f <$> pure x = pure (f x)
@[simp]
theorem FreeMagma.map_mul' {α β : Type u} (f : αβ) (x y : FreeMagma α) :
f <$> (x * y) = f <$> x * f <$> y
@[simp]
theorem FreeAddMagma.map_add' {α β : Type u} (f : αβ) (x y : FreeAddMagma α) :
f <$> (x + y) = f <$> x + f <$> y
@[simp]
theorem FreeMagma.pure_bind {α β : Type u} (f : αFreeMagma β) (x : α) :
pure x >>= f = f x
@[simp]
theorem FreeAddMagma.pure_bind {α β : Type u} (f : αFreeAddMagma β) (x : α) :
pure x >>= f = f x
@[simp]
theorem FreeMagma.mul_bind {α β : Type u} (f : αFreeMagma β) (x y : FreeMagma α) :
x * y >>= f = (x >>= f) * (y >>= f)
@[simp]
theorem FreeAddMagma.add_bind {α β : Type u} (f : αFreeAddMagma β) (x y : FreeAddMagma α) :
x + y >>= f = (x >>= f) + (y >>= f)
@[simp]
theorem FreeMagma.pure_seq {α β : Type u} {f : αβ} {x : FreeMagma α} :
pure f <*> x = f <$> x
@[simp]
theorem FreeAddMagma.pure_seq {α β : Type u} {f : αβ} {x : FreeAddMagma α} :
pure f <*> x = f <$> x
@[simp]
theorem FreeMagma.mul_seq {α β : Type u} {f g : FreeMagma (αβ)} {x : FreeMagma α} :
f * g <*> x = (f <*> x) * (g <*> x)
@[simp]
theorem FreeAddMagma.add_seq {α β : Type u} {f g : FreeAddMagma (αβ)} {x : FreeAddMagma α} :
f + g <*> x = (f <*> x) + (g <*> x)
def FreeMagma.traverse {m : Type u → Type u} [Applicative m] {α β : Type u} (F : αm β) :
FreeMagma αm (FreeMagma β)

FreeMagma is traversable.

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

FreeAddMagma is traversable.

Equations
@[simp]
theorem FreeMagma.traverse_pure {α β : 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} {m : Type u → Type u} [Applicative m] (F : αm β) (x : α) :
traverse F (pure x) = pure <$> F x
@[simp]
theorem FreeMagma.traverse_pure' {α β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) :
traverse F pure = fun (x : α) => pure <$> F x
@[simp]
theorem FreeAddMagma.traverse_pure' {α β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) :
traverse F pure = fun (x : α) => pure <$> F x
@[simp]
theorem FreeMagma.traverse_mul {α β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) (x y : FreeMagma α) :
traverse F (x * y) = (fun (x1 x2 : FreeMagma β) => x1 * x2) <$> traverse F x <*> traverse F y
@[simp]
theorem FreeAddMagma.traverse_add {α β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) (x y : FreeAddMagma α) :
traverse F (x + y) = (fun (x1 x2 : FreeAddMagma β) => x1 + x2) <$> traverse F x <*> traverse F y
@[simp]
theorem FreeMagma.traverse_mul' {α β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) :
Function.comp (traverse F) HMul.hMul = fun (x y : FreeMagma α) => (fun (x1 x2 : FreeMagma β) => x1 * x2) <$> traverse F x <*> traverse F y
@[simp]
theorem FreeAddMagma.traverse_add' {α β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) :
Function.comp (traverse F) HAdd.hAdd = fun (x y : FreeAddMagma α) => (fun (x1 x2 : FreeAddMagma β) => x1 + x2) <$> traverse F x <*> traverse F y
@[simp]
theorem FreeMagma.traverse_eq {α β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) (x : FreeMagma α) :
@[simp]
theorem FreeAddMagma.traverse_eq {α β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) (x : FreeAddMagma α) :
theorem FreeMagma.mul_map_seq {α : Type u} (x y : FreeMagma α) :
(fun (x1 x2 : FreeMagma α) => x1 * x2) <$> x <*> y = x * y
theorem FreeAddMagma.add_map_seq {α : Type u} (x y : FreeAddMagma α) :
(fun (x1 x2 : FreeAddMagma α) => x1 + x2) <$> x <*> y = x + y
def FreeMagma.repr {α : Type u} [Repr α] :

Representation of an element of a free magma.

Equations

Representation of an element of a free additive magma.

Equations
instance instReprFreeMagma {α : Type u} [Repr α] :
Equations
instance instReprFreeAddMagma {α : Type u} [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
theorem FreeMagma.length_pos {α : Type u} (x : FreeMagma α) :
0 < x.length

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

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

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

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

Associativity relations for an additive magma.

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

Associativity relations for a magma.

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

Semigroup quotient of a magma.

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

Additive semigroup quotient of an additive magma.

Equations
theorem Magma.AssocQuotient.quot_mk_assoc {α : Type u} [Mul α] (x y z : α) :
Quot.mk (AssocRel α) (x * y * z) = Quot.mk (AssocRel α) (x * (y * z))
theorem AddMagma.FreeAddSemigroup.quot_mk_assoc {α : Type u} [Add α] (x y z : α) :
Quot.mk (AssocRel α) (x + y + z) = Quot.mk (AssocRel α) (x + (y + z))
theorem Magma.AssocQuotient.quot_mk_assoc_left {α : Type u} [Mul α] (x y z w : α) :
Quot.mk (AssocRel α) (x * (y * z * w)) = Quot.mk (AssocRel α) (x * (y * (z * w)))
theorem AddMagma.FreeAddSemigroup.quot_mk_assoc_left {α : Type u} [Add α] (x y z w : α) :
Quot.mk (AssocRel α) (x + (y + z + w)) = Quot.mk (AssocRel α) (x + (y + (z + w)))

Embedding from magma to its free semigroup.

Equations

Embedding from additive magma to its free additive semigroup.

Equations
theorem Magma.AssocQuotient.induction_on {α : Type u} [Mul α] {C : AssocQuotient αProp} (x : AssocQuotient α) (ih : ∀ (x : α), C (of x)) :
C x
theorem AddMagma.FreeAddSemigroup.induction_on {α : Type u} [Add α] {C : FreeAddSemigroup αProp} (x : FreeAddSemigroup α) (ih : ∀ (x : α), C (of x)) :
C x
theorem AddMagma.FreeAddSemigroup.hom_ext {α : Type u} [Add α] {β : Type v} [AddSemigroup β] {f g : FreeAddSemigroup α →ₙ+ β} (h : f.comp of = g.comp of) :
f = g
theorem Magma.AssocQuotient.hom_ext {α : Type u} [Mul α] {β : Type v} [Semigroup β] {f g : AssocQuotient α →ₙ* β} (h : f.comp of = g.comp of) :
f = g
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.

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

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

Equations

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

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

structure FreeSemigroup (α : Type u) :

Free semigroup over a given alphabet.

  • head : α

    The head of the element

  • tail : List α

    The tail of the element

theorem FreeSemigroup.ext {α : Type u} {x y : FreeSemigroup α} (head : x.head = y.head) (tail : x.tail = y.tail) :
x = y
theorem FreeAddSemigroup.ext {α : Type u} {x y : FreeAddSemigroup α} (head : x.head = y.head) (tail : x.tail = y.tail) :
x = y
@[simp]
theorem FreeSemigroup.head_mul {α : Type u} (x y : FreeSemigroup α) :
(x * y).head = x.head
@[simp]
theorem FreeAddSemigroup.head_add {α : Type u} (x y : FreeAddSemigroup α) :
(x + y).head = x.head
@[simp]
theorem FreeSemigroup.tail_mul {α : Type u} (x y : FreeSemigroup α) :
(x * y).tail = x.tail ++ y.head :: y.tail
@[simp]
theorem FreeAddSemigroup.tail_add {α : Type u} (x y : FreeAddSemigroup α) :
(x + y).tail = x.tail ++ y.head :: y.tail
@[simp]
theorem FreeSemigroup.mk_mul_mk {α : Type u} (x y : α) (L1 L2 : List α) :
{ head := x, tail := L1 } * { head := y, tail := L2 } = { head := x, tail := L1 ++ y :: L2 }
@[simp]
theorem FreeAddSemigroup.mk_add_mk {α : Type u} (x y : α) (L1 L2 : List α) :
{ head := x, tail := L1 } + { head := y, tail := L2 } = { head := x, tail := L1 ++ y :: L2 }
def FreeSemigroup.of {α : Type u} (x : α) :

The embedding α → FreeSemigroup α.

Equations
def FreeAddSemigroup.of {α : Type u} (x : α) :

The embedding α → FreeAddSemigroup α.

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

Length of an element of free semigroup.

Equations

Length of an element of free additive semigroup

Equations
@[simp]
theorem FreeSemigroup.length_mul {α : Type u} (x y : FreeSemigroup α) :
(x * y).length = x.length + y.length
@[simp]
theorem FreeAddSemigroup.length_add {α : Type u} (x y : FreeAddSemigroup α) :
(x + y).length = x.length + y.length
@[simp]
theorem FreeSemigroup.length_of {α : Type u} (x : α) :
(of x).length = 1
@[simp]
theorem FreeAddSemigroup.length_of {α : Type u} (x : α) :
(of x).length = 1
def FreeSemigroup.recOnMul {α : Type u} {C : FreeSemigroup αSort l} (x : FreeSemigroup α) (ih1 : (x : α) → C (of x)) (ih2 : (x : α) → (y : FreeSemigroup α) → C (of x)C yC (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.
def FreeAddSemigroup.recOnAdd {α : Type u} {C : FreeAddSemigroup αSort l} (x : FreeAddSemigroup α) (ih1 : (x : α) → C (of x)) (ih2 : (x : α) → (y : FreeAddSemigroup α) → C (of x)C yC (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.
theorem FreeAddSemigroup.hom_ext {α : Type u} {β : Type v} [Add β] {f g : FreeAddSemigroup α →ₙ+ β} (h : f of = g of) :
f = g
theorem FreeSemigroup.hom_ext {α : Type u} {β : Type v} [Mul β] {f g : FreeSemigroup α →ₙ* β} (h : f of = g of) :
f = g
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.
def FreeAddSemigroup.lift {α : Type u} {β : Type v} [AddSemigroup β] :
(αβ) (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.
@[simp]
theorem FreeSemigroup.lift_symm_apply {α : Type u} {β : Type v} [Semigroup β] (f : FreeSemigroup α →ₙ* β) (a✝ : α) :
lift.symm f a✝ = (f of) a✝
@[simp]
theorem FreeAddSemigroup.lift_symm_apply {α : Type u} {β : Type v} [AddSemigroup β] (f : FreeAddSemigroup α →ₙ+ β) (a✝ : α) :
lift.symm f a✝ = (f of) a✝
@[simp]
theorem FreeSemigroup.lift_of {α : Type u} {β : Type v} [Semigroup β] (f : αβ) (x : α) :
(lift f) (of x) = f x
@[simp]
theorem FreeAddSemigroup.lift_of {α : Type u} {β : Type v} [AddSemigroup β] (f : αβ) (x : α) :
(lift f) (of x) = f x
@[simp]
theorem FreeSemigroup.lift_comp_of {α : Type u} {β : Type v} [Semigroup β] (f : αβ) :
(lift f) of = f
@[simp]
theorem FreeAddSemigroup.lift_comp_of {α : Type u} {β : Type v} [AddSemigroup β] (f : αβ) :
(lift f) of = f
@[simp]
theorem FreeSemigroup.lift_comp_of' {α : Type u} {β : Type v} [Semigroup β] (f : FreeSemigroup α →ₙ* β) :
lift (f of) = f
@[simp]
theorem FreeAddSemigroup.lift_comp_of' {α : Type u} {β : Type v} [AddSemigroup β] (f : FreeAddSemigroup α →ₙ+ β) :
lift (f of) = f
theorem FreeSemigroup.lift_of_mul {α : Type u} {β : Type v} [Semigroup β] (f : αβ) (x : α) (y : FreeSemigroup α) :
(lift f) (of x * y) = f x * (lift f) y
theorem FreeAddSemigroup.lift_of_add {α : Type u} {β : Type v} [AddSemigroup β] (f : αβ) (x : α) (y : FreeAddSemigroup α) :
(lift f) (of x + y) = f x + (lift f) y
def FreeSemigroup.map {α : Type u} {β : Type v} (f : αβ) :

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

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

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

Equations
@[simp]
theorem FreeSemigroup.map_of {α : Type u} {β : Type v} (f : αβ) (x : α) :
(map f) (of x) = of (f x)
@[simp]
theorem FreeAddSemigroup.map_of {α : Type u} {β : Type v} (f : αβ) (x : α) :
(map f) (of x) = of (f x)
@[simp]
theorem FreeSemigroup.length_map {α : Type u} {β : Type v} (f : αβ) (x : FreeSemigroup α) :
((map f) x).length = x.length
@[simp]
theorem FreeAddSemigroup.length_map {α : Type u} {β : Type v} (f : αβ) (x : FreeAddSemigroup α) :
((map f) x).length = x.length
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
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
@[simp]
theorem FreeSemigroup.map_pure {α β : Type u} (f : αβ) (x : α) :
f <$> pure x = pure (f x)
@[simp]
theorem FreeAddSemigroup.map_pure {α β : Type u} (f : αβ) (x : α) :
f <$> pure x = pure (f x)
@[simp]
theorem FreeSemigroup.map_mul' {α β : Type u} (f : αβ) (x y : FreeSemigroup α) :
f <$> (x * y) = f <$> x * f <$> y
@[simp]
theorem FreeAddSemigroup.map_add' {α β : Type u} (f : αβ) (x y : FreeAddSemigroup α) :
f <$> (x + y) = f <$> x + f <$> y
@[simp]
theorem FreeSemigroup.pure_bind {α β : Type u} (f : αFreeSemigroup β) (x : α) :
pure x >>= f = f x
@[simp]
theorem FreeAddSemigroup.pure_bind {α β : Type u} (f : αFreeAddSemigroup β) (x : α) :
pure x >>= f = f x
@[simp]
theorem FreeSemigroup.mul_bind {α β : Type u} (f : αFreeSemigroup β) (x y : FreeSemigroup α) :
x * y >>= f = (x >>= f) * (y >>= f)
@[simp]
theorem FreeAddSemigroup.add_bind {α β : Type u} (f : αFreeAddSemigroup β) (x y : FreeAddSemigroup α) :
x + y >>= f = (x >>= f) + (y >>= f)
@[simp]
theorem FreeSemigroup.pure_seq {α β : Type u} {f : αβ} {x : FreeSemigroup α} :
pure f <*> x = f <$> x
@[simp]
theorem FreeAddSemigroup.pure_seq {α β : Type u} {f : αβ} {x : FreeAddSemigroup α} :
pure f <*> x = f <$> x
@[simp]
theorem FreeSemigroup.mul_seq {α β : Type u} {f g : FreeSemigroup (αβ)} {x : FreeSemigroup α} :
f * g <*> x = (f <*> x) * (g <*> x)
@[simp]
theorem FreeAddSemigroup.add_seq {α β : Type u} {f g : FreeAddSemigroup (αβ)} {x : FreeAddSemigroup α} :
f + g <*> x = (f <*> x) + (g <*> x)
def FreeSemigroup.traverse {m : Type u → Type u} [Applicative m] {α β : Type u} (F : αm β) (x : FreeSemigroup α) :

FreeSemigroup is traversable.

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

FreeAddSemigroup is traversable.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem FreeSemigroup.traverse_pure {α β : 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} {m : Type u → Type u} [Applicative m] (F : αm β) (x : α) :
traverse F (pure x) = pure <$> F x
@[simp]
theorem FreeSemigroup.traverse_pure' {α β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) :
traverse F pure = fun (x : α) => pure <$> F x
@[simp]
theorem FreeAddSemigroup.traverse_pure' {α β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) :
traverse F pure = fun (x : α) => pure <$> F x
@[simp]
theorem FreeSemigroup.traverse_mul {α β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) [LawfulApplicative m] (x y : FreeSemigroup α) :
traverse F (x * y) = (fun (x1 x2 : FreeSemigroup β) => x1 * x2) <$> traverse F x <*> traverse F y
@[simp]
theorem FreeAddSemigroup.traverse_add {α β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) [LawfulApplicative m] (x y : FreeAddSemigroup α) :
traverse F (x + y) = (fun (x1 x2 : FreeAddSemigroup β) => x1 + x2) <$> traverse F x <*> traverse F y
@[simp]
theorem FreeSemigroup.traverse_mul' {α β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) [LawfulApplicative m] :
Function.comp (traverse F) HMul.hMul = fun (x y : FreeSemigroup α) => (fun (x1 x2 : FreeSemigroup β) => x1 * x2) <$> traverse F x <*> traverse F y
@[simp]
theorem FreeAddSemigroup.traverse_add' {α β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) [LawfulApplicative m] :
Function.comp (traverse F) HAdd.hAdd = fun (x y : FreeAddSemigroup α) => (fun (x1 x2 : FreeAddSemigroup β) => x1 + x2) <$> traverse F x <*> traverse F y
@[simp]
theorem FreeSemigroup.traverse_eq {α β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) (x : FreeSemigroup α) :
@[simp]
theorem FreeAddSemigroup.traverse_eq {α β : Type u} {m : Type u → Type u} [Applicative m] (F : αm β) (x : FreeAddSemigroup α) :
theorem FreeSemigroup.mul_map_seq {α : Type u} (x y : FreeSemigroup α) :
(fun (x1 x2 : FreeSemigroup α) => x1 * x2) <$> x <*> y = x * y
theorem FreeAddSemigroup.add_map_seq {α : Type u} (x y : FreeAddSemigroup α) :
(fun (x1 x2 : FreeAddSemigroup α) => x1 + x2) <$> x <*> y = x + y
Equations
Equations
theorem FreeMagma.toFreeSemigroup_map {α : Type u} {β : Type v} (f : αβ) (x : FreeMagma α) :