Free constructions

Main definitions

• FreeMagma α: free magma (structure with binary operation without any axioms) over alphabet α, defined inductively, with traversable instance and decidable equality.
• MagmaAssocQuotient α: quotient of a magma α by the associativity equivalence relation.
• FreeSemigroup α: 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.
• FreeMagmaAssocQuotientEquiv α: isomorphism between MagmaAssocQuotient (FreeMagma α) and FreeSemigroup α.
• FreeMagma.lift: the universal property of the free magma, expressing its adjointness.

inductive FreeAddMagma (α : Type u) : Type u

If α is a type, then FreeAddMagma α is the free additive magma generated by α. This is an additive magma equipped with a function FreeAddMagma.of : α → FreeAddMagma α which has the following universal property: if M is any magma, and f : α → M is any function, then this function is the composite of FreeAddMagma.of and a unique additive homomorphism FreeAddMagma.lift f : FreeAddMagma α →ₙ+ M.

A typical element of FreeAddMagma α is a formal non-associative sum of elements of α. For example if x and y are terms of type α then x + ((y + y) + x) is a "typical" element of FreeAddMagma α. One can think of FreeAddMagma α as the type of binary trees with leaves labelled by α. In general, no pair of distinct elements in FreeAddMagma α will commute.

• of {α : Type u} : α → FreeAddMagma α
• add {α : Type u} : FreeAddMagma α → FreeAddMagma α → FreeAddMagma α

instance instDecidableEqFreeAddMagma {α✝ : Type u_1} [DecidableEq α✝] : DecidableEq (FreeAddMagma α✝)

Equations

• instDecidableEqFreeAddMagma = instDecidableEqFreeAddMagma.decEq

def instDecidableEqFreeAddMagma.decEq {α✝ : Type u_1} [DecidableEq α✝] (x✝ x✝¹ : FreeAddMagma α✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• instDecidableEqFreeAddMagma.decEq (FreeAddMagma.of a) (FreeAddMagma.of b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• instDecidableEqFreeAddMagma.decEq (FreeAddMagma.of a) (a_1.add a_2) = isFalse ⋯
• instDecidableEqFreeAddMagma.decEq (a.add a_1) (FreeAddMagma.of a_2) = isFalse ⋯

inductive FreeMagma (α : Type u) : Type u

If α is a type, then FreeMagma α is the free magma generated by α. This is a magma equipped with a function FreeMagma.of : α → FreeMagma α which has the following universal property: if M is any magma, and f : α → M is any function, then this function is the composite of FreeMagma.of and a unique multiplicative homomorphism FreeMagma.lift f : FreeMagma α →ₙ* M.

A typical element of FreeMagma α is a formal non-associative product of elements of α. For example if x and y are terms of type α then x * ((y * y) * x) is a "typical" element of FreeMagma α. One can think of FreeMagma α as the type of binary trees with leaves labelled by α. In general, no pair of distinct elements in FreeMagma α will commute.

• of {α : Type u} : α → FreeMagma α
• mul {α : Type u} : FreeMagma α → FreeMagma α → FreeMagma α

def instDecidableEqFreeMagma.decEq {α✝ : Type u_1} [DecidableEq α✝] (x✝ x✝¹ : FreeMagma α✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• instDecidableEqFreeMagma.decEq (FreeMagma.of a) (FreeMagma.of b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• instDecidableEqFreeMagma.decEq (FreeMagma.of a) (a_1.mul a_2) = isFalse ⋯
• instDecidableEqFreeMagma.decEq (a.mul a_1) (FreeMagma.of a_2) = isFalse ⋯

instance instDecidableEqFreeMagma {α✝ : Type u_1} [DecidableEq α✝] : DecidableEq (FreeMagma α✝)

Equations

• instDecidableEqFreeMagma = instDecidableEqFreeMagma.decEq

instance FreeMagma.instInhabited {α : Type u} [Inhabited α] : Inhabited (FreeMagma α)

Equations

• FreeMagma.instInhabited = { default := FreeMagma.of default }

instance FreeAddMagma.instInhabited {α : Type u} [Inhabited α] : Inhabited (FreeAddMagma α)

Equations

• FreeAddMagma.instInhabited = { default := FreeAddMagma.of default }

instance FreeMagma.instMul {α : Type u} : Mul (FreeMagma α)

Equations

• FreeMagma.instMul = { mul := FreeMagma.mul }

instance FreeAddMagma.instAdd {α : Type u} : Add (FreeAddMagma α)

Equations

• FreeAddMagma.instAdd = { add := FreeAddMagma.add }

@[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 x → C y → C (x * y)) : C x

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

Equations

• x.recOnMul ih1 ih2 = FreeMagma.recOn x ih1 ih2

def FreeAddMagma.recOnAdd {α : Type u} {C : FreeAddMagma α → Sort l} (x : FreeAddMagma α) (ih1 : (x : α) → C (of x)) (ih2 : (x y : FreeAddMagma α) → C x → C y → C (x + y)) : C x

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

Equations

• x.recOnAdd ih1 ih2 = FreeAddMagma.recOn x ih1 ih2

theorem FreeMagma.hom_ext {α : Type u} {β : Type v} [Mul β] {f g : FreeMagma α →ₙ* β} (h : ⇑f ∘ of = ⇑g ∘ of) : f = g

theorem FreeAddMagma.hom_ext {α : Type u} {β : Type v} [Add β] {f g : FreeAddMagma α →ₙ+ β} (h : ⇑f ∘ of = ⇑g ∘ of) : f = g

theorem FreeMagma.hom_ext_iff {α : Type u} {β : Type v} [Mul β] {f g : FreeMagma α →ₙ* β} : f = g ↔ ⇑f ∘ of = ⇑g ∘ of

theorem FreeAddMagma.hom_ext_iff {α : Type u} {β : Type v} [Add β] {f g : FreeAddMagma α →ₙ+ β} : f = g ↔ ⇑f ∘ of = ⇑g ∘ of

def FreeMagma.liftAux {α : Type u} {β : Type v} [Mul β] (f : α → β) : FreeMagma α → β

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

Equations

• FreeMagma.liftAux f (FreeMagma.of x_1) = f x_1
• FreeMagma.liftAux f (x_1.mul y) = FreeMagma.liftAux f x_1 * FreeMagma.liftAux f y

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

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

Equations

• FreeAddMagma.liftAux f (FreeAddMagma.of x_1) = f x_1
• FreeAddMagma.liftAux f (x_1.add y) = FreeAddMagma.liftAux f x_1 + FreeAddMagma.liftAux f y

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 := ⋯ }

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 : α → β) : FreeMagma α →ₙ* FreeMagma β

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

Equations

• FreeMagma.map f = FreeMagma.lift (FreeMagma.of ∘ f)

def FreeAddMagma.map {α : Type u} {β : Type v} (f : α → β) : FreeAddMagma α →ₙ+ FreeAddMagma β

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

Equations

• FreeAddMagma.map f = FreeAddMagma.lift (FreeAddMagma.of ∘ f)

@[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)

instance FreeMagma.instMonad : Monad FreeMagma

Equations

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

instance FreeAddMagma.instMonad : Monad FreeAddMagma

Equations

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

def FreeMagma.recOnPure {α : Type u} {C : FreeMagma α → Sort l} (x : FreeMagma α) (ih1 : (x : α) → C (pure x)) (ih2 : (x y : FreeMagma α) → C x → C y → C (x * y)) : C x

Recursor on FreeMagma using pure instead of of.

Equations

• x.recOnPure ih1 ih2 = x.recOnMul ih1 ih2

def FreeAddMagma.recOnPure {α : Type u} {C : FreeAddMagma α → Sort l} (x : FreeAddMagma α) (ih1 : (x : α) → C (pure x)) (ih2 : (x y : FreeAddMagma α) → C x → C y → C (x + y)) : C x

Recursor on FreeAddMagma using pure instead of of.

Equations

• x.recOnPure ih1 ih2 = x.recOnAdd ih1 ih2

@[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)

instance FreeMagma.instLawfulMonad : LawfulMonad FreeMagma

instance FreeAddMagma.instLawfulMonad : LawfulMonad FreeAddMagma

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

FreeMagma is traversable.

Equations

• FreeMagma.traverse F (FreeMagma.of x_1) = FreeMagma.of <$> F x_1
• FreeMagma.traverse F (x_1.mul y) = (fun (x1 x2 : FreeMagma β) => x1 * x2) <$> FreeMagma.traverse F x_1 <*> FreeMagma.traverse F y

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

FreeAddMagma is traversable.

Equations

• FreeAddMagma.traverse F (FreeAddMagma.of x_1) = FreeAddMagma.of <$> F x_1
• FreeAddMagma.traverse F (x_1.add y) = (fun (x1 x2 : FreeAddMagma β) => x1 + x2) <$> FreeAddMagma.traverse F x_1 <*> FreeAddMagma.traverse F y

instance FreeMagma.instTraversable : Traversable FreeMagma

Equations

• FreeMagma.instTraversable = { toFunctor := FreeMagma.instMonad.toFunctor, traverse := @FreeMagma.traverse }

instance FreeAddMagma.instTraversable : Traversable FreeAddMagma

Equations

• FreeAddMagma.instTraversable = { toFunctor := FreeAddMagma.instMonad.toFunctor, traverse := @FreeAddMagma.traverse }

@[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 α) : FreeMagma.traverse F x = traverse F x

@[simp]

theorem FreeAddMagma.traverse_eq {α β : Type u} {m : Type u → Type u} [Applicative m] (F : α → m β) (x : FreeAddMagma α) : FreeAddMagma.traverse F x = traverse F x

@[deprecated "Use map_pure and seq_pure" (since := "2025-05-21")]

theorem FreeMagma.mul_map_seq {α : Type u} (x y : FreeMagma α) : (fun (x1 x2 : FreeMagma α) => x1 * x2) <$> x <*> y = x * y

@[deprecated "Use map_pure and seq_pure" (since := "2025-05-21")]

theorem FreeAddMagma.add_map_seq {α : Type u} (x y : FreeAddMagma α) : (fun (x1 x2 : FreeAddMagma α) => x1 + x2) <$> x <*> y = x + y

instance FreeMagma.instLawfulTraversable : LawfulTraversable FreeMagma

instance FreeAddMagma.instLawfulTraversable : LawfulTraversable FreeAddMagma

def FreeMagma.repr {α : Type u} [Repr α] : FreeMagma α → Std.Format

Representation of an element of a free magma.

Equations

• (FreeMagma.of x_1).repr = repr x_1
• (x_1.mul y).repr = Std.Format.text "( " ++ x_1.repr ++ Std.Format.text " * " ++ y.repr ++ Std.Format.text " )"

def FreeAddMagma.repr {α : Type u} [Repr α] : FreeAddMagma α → Std.Format

Representation of an element of a free additive magma.

Equations

• (FreeAddMagma.of x_1).repr = repr x_1
• (x_1.add y).repr = Std.Format.text "( " ++ x_1.repr ++ Std.Format.text " + " ++ y.repr ++ Std.Format.text " )"

instance instReprFreeMagma {α : Type u} [Repr α] : Repr (FreeMagma α)

Equations

• instReprFreeMagma = { reprPrec := fun (o : FreeMagma α) (x : ℕ) => o.repr }

instance instReprFreeAddMagma {α : Type u} [Repr α] : Repr (FreeAddMagma α)

Equations

• instReprFreeAddMagma = { reprPrec := fun (o : FreeAddMagma α) (x : ℕ) => o.repr }

def FreeMagma.length {α : Type u} : FreeMagma α → ℕ

Length of an element of a free magma.

Equations

• (FreeMagma.of x_1).length = 1
• (x_1.mul y).length = x_1.length + y.length

def FreeAddMagma.length {α : Type u} : FreeAddMagma α → ℕ

Length of an element of a free additive magma.

Equations

• (FreeAddMagma.of x_1).length = 1
• (x_1.add y).length = x_1.length + y.length

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.

• intro {α : Type u} [Add α] (x y z : α) : AssocRel α (x + y + z) (x + (y + z))
• left {α : Type u} [Add α] (w x y z : α) : AssocRel α (w + (x + y + z)) (w + (x + (y + z)))

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

Associativity relations for a magma.

• intro {α : Type u} [Mul α] (x y z : α) : AssocRel α (x * y * z) (x * (y * z))
• left {α : Type u} [Mul α] (w x y z : α) : AssocRel α (w * (x * y * z)) (w * (x * (y * z)))

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

Semigroup quotient of a magma.

Equations

• Magma.AssocQuotient α = Quot (Magma.AssocRel α)

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

Additive semigroup quotient of an additive magma.

Equations

• AddMagma.FreeAddSemigroup α = Quot (AddMagma.AssocRel α)

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)))

instance Magma.AssocQuotient.instSemigroup {α : Type u} [Mul α] : Semigroup (AssocQuotient α)

Equations

• Magma.AssocQuotient.instSemigroup = { mul := fun (x y : Magma.AssocQuotient α) => Quot.liftOn₂ x y (fun (x y : α) => Quot.mk (Magma.AssocRel α) (x * y)) ⋯ ⋯, mul_assoc := ⋯ }

instance AddMagma.FreeAddSemigroup.instAddSemigroup {α : Type u} [Add α] : AddSemigroup (FreeAddSemigroup α)

Equations

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

def Magma.AssocQuotient.of {α : Type u} [Mul α] : α →ₙ* AssocQuotient α

Embedding from magma to its free semigroup.

Equations

• Magma.AssocQuotient.of = { toFun := Quot.mk (Magma.AssocRel α), map_mul' := ⋯ }

def AddMagma.FreeAddSemigroup.of {α : Type u} [Add α] : α →ₙ+ FreeAddSemigroup α

Embedding from additive magma to its free additive semigroup.

Equations

• AddMagma.FreeAddSemigroup.of = { toFun := Quot.mk (AddMagma.AssocRel α), map_add' := ⋯ }

instance Magma.AssocQuotient.instInhabited {α : Type u} [Mul α] [Inhabited α] : Inhabited (AssocQuotient α)

Equations

• Magma.AssocQuotient.instInhabited = { default := Magma.AssocQuotient.of default }

instance AddMagma.FreeAddSemigroup.instInhabited {α : Type u} [Add α] [Inhabited α] : Inhabited (FreeAddSemigroup α)

Equations

• AddMagma.FreeAddSemigroup.instInhabited = { default := AddMagma.FreeAddSemigroup.of default }

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 Magma.AssocQuotient.hom_ext {α : Type u} [Mul α] {β : Type v} [Semigroup β] {f g : AssocQuotient α →ₙ* β} (h : f.comp of = g.comp of) : f = g

theorem AddMagma.FreeAddSemigroup.hom_ext {α : Type u} [Add α] {β : Type v} [AddSemigroup β] {f g : FreeAddSemigroup α →ₙ+ β} (h : f.comp of = g.comp of) : f = g

theorem AddMagma.FreeAddSemigroup.hom_ext_iff {α : Type u} [Add α] {β : Type v} [AddSemigroup β] {f g : FreeAddSemigroup α →ₙ+ β} : f = g ↔ f.comp of = g.comp of

theorem Magma.AssocQuotient.hom_ext_iff {α : Type u} [Mul α] {β : Type v} [Semigroup β] {f g : AssocQuotient α →ₙ* β} : f = g ↔ f.comp of = g.comp of

def Magma.AssocQuotient.lift {α : Type u} [Mul α] {β : Type v} [Semigroup β] : (α →ₙ* β) ≃ (AssocQuotient α →ₙ* β)

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.

def AddMagma.FreeAddSemigroup.lift {α : Type u} [Add α] {β : Type v} [AddSemigroup β] : (α →ₙ+ β) ≃ (FreeAddSemigroup α →ₙ+ β)

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} [Add α] {β : Type v} [AddSemigroup β] (f : FreeAddSemigroup α →ₙ+ β) : lift.symm f = f.comp of

@[simp]

theorem Magma.AssocQuotient.lift_symm_apply {α : Type u} [Mul α] {β : Type v} [Semigroup β] (f : AssocQuotient α →ₙ* β) : lift.symm f = f.comp of

@[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 : α →ₙ* β) : AssocQuotient α →ₙ* AssocQuotient β

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

Equations

• Magma.AssocQuotient.map f = Magma.AssocQuotient.lift (Magma.AssocQuotient.of.comp f)

def AddMagma.FreeAddSemigroup.map {α : Type u} [Add α] {β : Type v} [Add β] (f : α →ₙ+ β) : FreeAddSemigroup α →ₙ+ FreeAddSemigroup β

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

Equations

• AddMagma.FreeAddSemigroup.map f = AddMagma.FreeAddSemigroup.lift (AddMagma.FreeAddSemigroup.of.comp f)

@[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) : Type u

If α is a type, then FreeAddSemigroup α is the free additive semigroup generated by α. This is an additive semigroup equipped with a function FreeAddSemigroup.of : α → FreeAddSemigroup α which has the following universal property: if M is any additive semigroup, and f : α → M is any function, then this function is the composite of FreeAddSemigroup.of and a unique semigroup homomorphism FreeAddSemigroup.lift f : FreeAddSemigroup α →ₙ+ M.

A typical element of FreeAddSemigroup α is a nonempty formal sum of elements of α. For example if x and y are terms of type α then x + y + y + x is a "typical" element of FreeAddSemigroup α. In particular if α is empty then FreeAddSemigroup α is also empty, and if α has one term then FreeAddSemigroup α is isomorphic to ℕ+. If α has two or more terms then FreeAddSemigroup α is not commutative. One can think of FreeAddSemigroup α as the type of nonempty lists of α, with addition given by concatenation.

• head : α

  The head of the element

• tail : List α

  The tail of the element

structure FreeSemigroup (α : Type u) : Type u

If α is a type, then FreeSemigroup α is the free semigroup generated by α. This is a semigroup equipped with a function FreeSemigroup.of : α → FreeSemigroup α which has the following universal property: if M is any semigroup, and f : α → M is any function, then this function is the composite of FreeSemigroup.of and a unique semigroup homomorphism FreeSemigroup.lift f : FreeSemigroup α →ₙ* M.

A typical element of FreeSemigroup α is a nonempty formal product of elements of α. For example if x and y are terms of type α then x * y * y * x is a "typical" element of FreeSemigroup α. In particular if α is empty then FreeSemigroup α is also empty, and if α has one term then FreeSemigroup α is isomorphic to Multiplicative ℕ+. If α has two or more terms then FreeSemigroup α is not commutative. One can think of FreeSemigroup α as the type of nonempty lists of α, with multiplication given by concatenation.

• head : α

  The head of the element

• tail : List α

  The tail of the element

theorem FreeAddSemigroup.ext_iff {α : Type u} {x y : FreeAddSemigroup α} : x = y ↔ x.head = y.head ∧ x.tail = y.tail

theorem FreeSemigroup.ext_iff {α : Type u} {x y : FreeSemigroup α} : x = y ↔ x.head = y.head ∧ x.tail = y.tail

theorem FreeAddSemigroup.ext {α : Type u} {x y : FreeAddSemigroup α} (head : x.head = y.head) (tail : x.tail = y.tail) : x = y

theorem FreeSemigroup.ext {α : Type u} {x y : FreeSemigroup α} (head : x.head = y.head) (tail : x.tail = y.tail) : x = y

instance FreeSemigroup.instSemigroup {α : Type u} : Semigroup (FreeSemigroup α)

Equations

• FreeSemigroup.instSemigroup = { mul := fun (L1 L2 : FreeSemigroup α) => { head := L1.head, tail := L1.tail ++ L2.head :: L2.tail }, mul_assoc := ⋯ }

instance FreeAddSemigroup.instAddSemigroup {α : Type u} : AddSemigroup (FreeAddSemigroup α)

Equations

• FreeAddSemigroup.instAddSemigroup = { add := fun (L1 L2 : FreeAddSemigroup α) => { head := L1.head, tail := L1.tail ++ L2.head :: L2.tail }, add_assoc := ⋯ }

@[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 : α) : FreeSemigroup α

The embedding α → FreeSemigroup α.

Equations

• FreeSemigroup.of x = { head := x, tail := [] }

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

The embedding α → FreeAddSemigroup α.

Equations

• FreeAddSemigroup.of x = { head := x, tail := [] }

@[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 = []

@[simp]

theorem FreeSemigroup.of_head {α : Type u} (x : α) : (of x).head = x

def FreeSemigroup.length {α : Type u} (x : FreeSemigroup α) : ℕ

Length of an element of free semigroup.

Equations

• x.length = x.tail.length + 1

def FreeAddSemigroup.length {α : Type u} (x : FreeAddSemigroup α) : ℕ

Length of an element of free additive semigroup

Equations

• x.length = x.tail.length + 1

@[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

instance FreeSemigroup.instInhabited {α : Type u} [Inhabited α] : Inhabited (FreeSemigroup α)

Equations

• FreeSemigroup.instInhabited = { default := FreeSemigroup.of default }

instance FreeAddSemigroup.instInhabited {α : Type u} [Inhabited α] : Inhabited (FreeAddSemigroup α)

Equations

• FreeAddSemigroup.instInhabited = { default := FreeAddSemigroup.of default }

def FreeSemigroup.recOnMul {α : Type u} {C : FreeSemigroup α → Sort l} (x : FreeSemigroup α) (ih1 : (x : α) → C (of x)) (ih2 : (x : α) → (y : FreeSemigroup α) → C (of x) → C y → C (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 y → C (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 FreeSemigroup.hom_ext {α : Type u} {β : Type v} [Mul β] {f g : FreeSemigroup α →ₙ* β} (h : ⇑f ∘ of = ⇑g ∘ of) : f = g

theorem FreeAddSemigroup.hom_ext {α : Type u} {β : Type v} [Add β] {f g : FreeAddSemigroup α →ₙ+ β} (h : ⇑f ∘ of = ⇑g ∘ of) : f = g

theorem FreeAddSemigroup.hom_ext_iff {α : Type u} {β : Type v} [Add β] {f g : FreeAddSemigroup α →ₙ+ β} : f = g ↔ ⇑f ∘ of = ⇑g ∘ of

theorem FreeSemigroup.hom_ext_iff {α : Type u} {β : Type v} [Mul β] {f g : FreeSemigroup α →ₙ* β} : f = g ↔ ⇑f ∘ of = ⇑g ∘ of

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 : α → β) : FreeSemigroup α →ₙ* FreeSemigroup β

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

Equations

• FreeSemigroup.map f = FreeSemigroup.lift (FreeSemigroup.of ∘ f)

def FreeAddSemigroup.map {α : Type u} {β : Type v} (f : α → β) : FreeAddSemigroup α →ₙ+ FreeAddSemigroup β

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

Equations

• FreeAddSemigroup.map f = FreeAddSemigroup.lift (FreeAddSemigroup.of ∘ f)

@[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

instance FreeSemigroup.instMonad : Monad FreeSemigroup

Equations

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

instance FreeAddSemigroup.instMonad : Monad FreeAddSemigroup

Equations

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

def FreeSemigroup.recOnPure {α : Type u} {C : FreeSemigroup α → Sort l} (x : FreeSemigroup α) (ih1 : (x : α) → C (pure x)) (ih2 : (x : α) → (y : FreeSemigroup α) → C (pure x) → C y → C (pure x * y)) : C x

Recursor that uses pure instead of of.

Equations

• x.recOnPure ih1 ih2 = x.recOnMul ih1 ih2

def FreeAddSemigroup.recOnPure {α : Type u} {C : FreeAddSemigroup α → Sort l} (x : FreeAddSemigroup α) (ih1 : (x : α) → C (pure x)) (ih2 : (x : α) → (y : FreeAddSemigroup α) → C (pure x) → C y → C (pure x + y)) : C x

Recursor that uses pure instead of of.

Equations

• x.recOnPure ih1 ih2 = x.recOnAdd ih1 ih2

@[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)

instance FreeSemigroup.instLawfulMonad : LawfulMonad FreeSemigroup

instance FreeAddSemigroup.instLawfulMonad : LawfulMonad FreeAddSemigroup

def FreeSemigroup.traverse {m : Type u → Type u} [Applicative m] {α β : Type u} (F : α → m β) (x : FreeSemigroup α) : m (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 α) : m (FreeAddSemigroup β)

FreeAddSemigroup is traversable.

Equations

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

instance FreeSemigroup.instTraversable : Traversable FreeSemigroup

Equations

• FreeSemigroup.instTraversable = { toFunctor := FreeSemigroup.instMonad.toFunctor, traverse := @FreeSemigroup.traverse }

instance FreeAddSemigroup.instTraversable : Traversable FreeAddSemigroup

Equations

• FreeAddSemigroup.instTraversable = { toFunctor := FreeAddSemigroup.instMonad.toFunctor, traverse := @FreeAddSemigroup.traverse }

@[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 α) : FreeSemigroup.traverse F x = traverse F x

@[simp]

theorem FreeAddSemigroup.traverse_eq {α β : Type u} {m : Type u → Type u} [Applicative m] (F : α → m β) (x : FreeAddSemigroup α) : FreeAddSemigroup.traverse F x = traverse F x

@[deprecated "Use map_pure and seq_pure" (since := "2025-05-21")]

theorem FreeSemigroup.mul_map_seq {α : Type u} (x y : FreeSemigroup α) : (fun (x1 x2 : FreeSemigroup α) => x1 * x2) <$> x <*> y = x * y

@[deprecated "Use map_pure and seq_pure" (since := "2025-05-21")]

theorem FreeAddSemigroup.add_map_seq {α : Type u} (x y : FreeAddSemigroup α) : (fun (x1 x2 : FreeAddSemigroup α) => x1 + x2) <$> x <*> y = x + y

instance FreeSemigroup.instLawfulTraversable : LawfulTraversable FreeSemigroup

instance FreeAddSemigroup.instLawfulTraversable : LawfulTraversable FreeAddSemigroup

instance FreeSemigroup.instDecidableEq {α : Type u} [DecidableEq α] : DecidableEq (FreeSemigroup α)

Equations

• x✝¹.instDecidableEq x✝ = decidable_of_iff' (x✝¹.head = x✝.head ∧ x✝¹.tail = x✝.tail) ⋯

instance FreeAddSemigroup.instDecidableEq {α : Type u} [DecidableEq α] : DecidableEq (FreeAddSemigroup α)

Equations

• x✝¹.instDecidableEq x✝ = decidable_of_iff' (x✝¹.head = x✝.head ∧ x✝¹.tail = x✝.tail) ⋯

def FreeMagma.toFreeSemigroup {α : Type u} : FreeMagma α →ₙ* FreeSemigroup α

The canonical multiplicative morphism from FreeMagma α to FreeSemigroup α.

Equations

• FreeMagma.toFreeSemigroup = FreeMagma.lift FreeSemigroup.of

def FreeAddMagma.toFreeAddSemigroup {α : Type u} : FreeAddMagma α →ₙ+ FreeAddSemigroup α

The canonical additive morphism from FreeAddMagma α to FreeAddSemigroup α.

Equations

• FreeAddMagma.toFreeAddSemigroup = FreeAddMagma.lift FreeAddSemigroup.of

@[simp]

theorem FreeMagma.toFreeSemigroup_of {α : Type u} (x : α) : toFreeSemigroup (of x) = FreeSemigroup.of x

@[simp]

theorem FreeAddMagma.toFreeAddSemigroup_of {α : Type u} (x : α) : toFreeAddSemigroup (of x) = FreeAddSemigroup.of x

@[simp]

theorem FreeMagma.toFreeSemigroup_comp_of {α : Type u} : ⇑toFreeSemigroup ∘ of = FreeSemigroup.of

@[simp]

theorem FreeAddMagma.toFreeAddSemigroup_comp_of {α : Type u} : ⇑toFreeAddSemigroup ∘ of = FreeAddSemigroup.of

theorem FreeMagma.toFreeSemigroup_comp_map {α : Type u} {β : Type v} (f : α → β) : toFreeSemigroup.comp (map f) = (FreeSemigroup.map f).comp toFreeSemigroup

theorem FreeAddMagma.toFreeAddSemigroup_comp_map {α : Type u} {β : Type v} (f : α → β) : toFreeAddSemigroup.comp (map f) = (FreeAddSemigroup.map f).comp toFreeAddSemigroup

theorem FreeMagma.toFreeSemigroup_map {α : Type u} {β : Type v} (f : α → β) (x : FreeMagma α) : toFreeSemigroup ((map f) x) = (FreeSemigroup.map f) (toFreeSemigroup x)

theorem FreeAddMagma.toFreeAddSemigroup_map {α : Type u} {β : Type v} (f : α → β) (x : FreeAddMagma α) : toFreeAddSemigroup ((map f) x) = (FreeAddSemigroup.map f) (toFreeAddSemigroup x)

@[simp]

theorem FreeMagma.length_toFreeSemigroup {α : Type u} (x : FreeMagma α) : (toFreeSemigroup x).length = x.length

@[simp]

theorem FreeAddMagma.length_toFreeAddSemigroup {α : Type u} (x : FreeAddMagma α) : (toFreeAddSemigroup x).length = x.length

def FreeMagmaAssocQuotientEquiv (α : Type u) : Magma.AssocQuotient (FreeMagma α) ≃* FreeSemigroup α

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

Equations

• FreeMagmaAssocQuotientEquiv α = (Magma.AssocQuotient.lift FreeMagma.toFreeSemigroup).toMulEquiv (FreeSemigroup.lift (⇑Magma.AssocQuotient.of ∘ FreeMagma.of)) ⋯ ⋯

def FreeAddMagmaAssocQuotientEquiv (α : Type u) : AddMagma.FreeAddSemigroup (FreeAddMagma α) ≃+ FreeAddSemigroup α

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

Equations

• FreeAddMagmaAssocQuotientEquiv α = (AddMagma.FreeAddSemigroup.lift FreeAddMagma.toFreeAddSemigroup).toAddEquiv (FreeAddSemigroup.lift (⇑AddMagma.FreeAddSemigroup.of ∘ FreeAddMagma.of)) ⋯ ⋯