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.

ink

inductive FreeAddMagma (α : Type u) : Type u

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

Free nonabelian additive magma over a given alphabet.

ink

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

Equations

• instDecidableEqFreeAddMagma = decEqFreeAddMagma✝

ink

inductive FreeMagma (α : Type u) : Type u

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

Free magma over a given alphabet.

ink

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

Equations

• instDecidableEqFreeMagma = decEqFreeMagma✝

ink

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

Equations

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

ink

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

Equations

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

ink

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

Equations

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

ink

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

Equations

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

ink

@[simp]

theorem FreeAddMagma.add_eq {α : Type u} (x : FreeAddMagma α) (y : FreeAddMagma α) : FreeAddMagma.add x y = x + y

ink

@[simp]

theorem FreeMagma.mul_eq {α : Type u} (x : FreeMagma α) (y : FreeMagma α) : FreeMagma.mul x y = x * y

ink

noncomputable def FreeAddMagma.recOnAdd {α : Type u} {C : FreeAddMagma α → Sort l} (x : FreeAddMagma α) (ih1 : (x : α) → C (FreeAddMagma.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

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

ink

noncomputable def FreeMagma.recOnMul {α : Type u} {C : FreeMagma α → Sort l} (x : FreeMagma α) (ih1 : (x : α) → C (FreeMagma.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

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

ink

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

ink

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

ink

def FreeMagma.liftAux {α : Type u} {β : Type v} [inst : 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 (FreeMagma.mul x_1 y) = FreeMagma.liftAux f x_1 * FreeMagma.liftAux f y

ink

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

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

ink

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.

ink

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.

ink

def FreeAddMagma.lift.proof_1 {α : Type u_1} {β : Type u_2} [inst : Add β] (f : α → β) (x : FreeAddMagma α) (y : FreeAddMagma α) : FreeAddMagma.liftAux f (x + y) = FreeAddMagma.liftAux f (x + y)

Equations

• (_ : FreeAddMagma.liftAux f (x + y) = FreeAddMagma.liftAux f (x + y)) = (_ : FreeAddMagma.liftAux f (x + y) = FreeAddMagma.liftAux f (x + y))

ink

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.

ink

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

ink

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

ink

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.

ink

@[simp]

theorem FreeAddMagma.lift_of {α : Type u} {β : Type v} [inst : Add β] (f : α → β) (x : α) : ↑(↑FreeAddMagma.lift f) (FreeAddMagma.of x) = f x

ink

@[simp]

theorem FreeMagma.lift_of {α : Type u} {β : Type v} [inst : Mul β] (f : α → β) (x : α) : ↑(↑FreeMagma.lift f) (FreeMagma.of x) = f x

ink

@[simp]

theorem FreeAddMagma.lift_comp_of {α : Type u} {β : Type v} [inst : Add β] (f : α → β) : ↑(↑FreeAddMagma.lift f) ∘ FreeAddMagma.of = f

ink

@[simp]

theorem FreeMagma.lift_comp_of {α : Type u} {β : Type v} [inst : Mul β] (f : α → β) : ↑(↑FreeMagma.lift f) ∘ FreeMagma.of = f

ink

@[simp]

theorem FreeAddMagma.lift_comp_of' {α : Type u} {β : Type v} [inst : Add β] (f : AddHom (FreeAddMagma α) β) : ↑FreeAddMagma.lift (↑f ∘ FreeAddMagma.of) = f

ink

@[simp]

theorem FreeMagma.lift_comp_of' {α : Type u} {β : Type v} [inst : Mul β] (f : FreeMagma α →ₙ* β) : ↑FreeMagma.lift (↑f ∘ FreeMagma.of) = f

ink

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

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

Equations

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

ink

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

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

Equations

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

ink

@[simp]

theorem FreeAddMagma.map_of {α : Type u} {β : Type v} (f : α → β) (x : α) : ↑(FreeAddMagma.map f) (FreeAddMagma.of x) = FreeAddMagma.of (f x)

ink

@[simp]

theorem FreeMagma.map_of {α : Type u} {β : Type v} (f : α → β) (x : α) : ↑(FreeMagma.map f) (FreeMagma.of x) = FreeMagma.of (f x)

ink

instance FreeAddMagma.instMonadFreeAddMagma : Monad FreeAddMagma

Equations

• FreeAddMagma.instMonadFreeAddMagma = Monad.mk

ink

instance FreeMagma.instMonadFreeMagma : Monad FreeMagma

Equations

• FreeMagma.instMonadFreeMagma = Monad.mk

ink

noncomputable 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

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

ink

noncomputable 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

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

ink

@[simp]

theorem FreeAddMagma.map_pure {α : Type u} {β : Type u} (f : α → β) (x : α) : f <$> pure x = pure (f x)

ink

@[simp]

theorem FreeMagma.map_pure {α : Type u} {β : Type u} (f : α → β) (x : α) : f <$> pure x = pure (f x)

ink

@[simp]

theorem FreeAddMagma.map_add' {α : Type u} {β : Type u} (f : α → β) (x : FreeAddMagma α) (y : FreeAddMagma α) : f <$> (x + y) = f <$> x + f <$> y

ink

@[simp]

theorem FreeMagma.map_mul' {α : Type u} {β : Type u} (f : α → β) (x : FreeMagma α) (y : FreeMagma α) : f <$> (x * y) = f <$> x * f <$> y

ink

@[simp]

theorem FreeAddMagma.pure_bind {α : Type u} {β : Type u} (f : α → FreeAddMagma β) (x : α) : pure x >>= f = f x

ink

@[simp]

theorem FreeMagma.pure_bind {α : Type u} {β : Type u} (f : α → FreeMagma β) (x : α) : pure x >>= f = f x

ink

@[simp]

theorem FreeAddMagma.add_bind {α : Type u} {β : Type u} (f : α → FreeAddMagma β) (x : FreeAddMagma α) (y : FreeAddMagma α) : x + y >>= f = (x >>= f) + (y >>= f)

ink

@[simp]

theorem FreeMagma.mul_bind {α : Type u} {β : Type u} (f : α → FreeMagma β) (x : FreeMagma α) (y : FreeMagma α) : x * y >>= f = (x >>= f) * (y >>= f)

ink

@[simp]

theorem FreeAddMagma.pure_seq {α : Type u} {β : Type u} {f : α → β} {x : FreeAddMagma α} : (Seq.seq (pure f) fun x => x) = f <$> x

ink

@[simp]

theorem FreeMagma.pure_seq {α : Type u} {β : Type u} {f : α → β} {x : FreeMagma α} : (Seq.seq (pure f) fun x => x) = f <$> x

ink

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

ink

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

ink

instance FreeAddMagma.instLawfulMonadFreeAddMagmaInstMonadFreeAddMagma : LawfulMonad FreeAddMagma

Equations

• FreeAddMagma.instLawfulMonadFreeAddMagmaInstMonadFreeAddMagma = FreeAddMagma.instLawfulMonadFreeAddMagmaInstMonadFreeAddMagma.proof_1

ink

def FreeAddMagma.instLawfulMonadFreeAddMagmaInstMonadFreeAddMagma.proof_1 : LawfulMonad FreeAddMagma

Equations

• FreeAddMagma.instLawfulMonadFreeAddMagmaInstMonadFreeAddMagma.proof_1 = (_ : LawfulMonad FreeAddMagma)

ink

instance FreeMagma.instLawfulMonadFreeMagmaInstMonadFreeMagma : LawfulMonad FreeMagma

Equations

• FreeMagma.instLawfulMonadFreeMagmaInstMonadFreeMagma = FreeMagma.instLawfulMonadFreeMagmaInstMonadFreeMagma.proof_1

ink

def FreeMagma.traverse {m : Type u → Type u} [inst : Applicative m] {α : Type u} {β : 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 (FreeMagma.mul x_1 y) = Seq.seq ((fun x x_1 => x * x_1) <$> FreeMagma.traverse F x_1) fun x => FreeMagma.traverse F y

ink

def FreeAddMagma.traverse {m : Type u → Type u} [inst : Applicative m] {α : Type u} {β : 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 (FreeAddMagma.add x_1 y) = Seq.seq ((fun x x_1 => x + x_1) <$> FreeAddMagma.traverse F x_1) fun x => FreeAddMagma.traverse F y

ink

instance FreeAddMagma.instTraversableFreeAddMagma : Traversable FreeAddMagma

Equations

• FreeAddMagma.instTraversableFreeAddMagma = Traversable.mk @FreeAddMagma.traverse

ink

instance FreeMagma.instTraversableFreeMagma : Traversable FreeMagma

Equations

• FreeMagma.instTraversableFreeMagma = Traversable.mk @FreeMagma.traverse

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

instance FreeAddMagma.instIsLawfulTraversableFreeAddMagmaInstTraversableFreeAddMagma : IsLawfulTraversable FreeAddMagma

Equations

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

ink

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.

ink

def FreeAddMagma.instIsLawfulTraversableFreeAddMagmaInstTraversableFreeAddMagma.proof_2 : ∀ {α : Type u_1} (x : FreeAddMagma α), traverse pure x = x

Equations

• (_ : traverse pure x = x) = (_ : traverse pure x = x)

ink

def FreeAddMagma.instIsLawfulTraversableFreeAddMagmaInstTraversableFreeAddMagma.proof_1 : LawfulFunctor FreeAddMagma

Equations

• FreeAddMagma.instIsLawfulTraversableFreeAddMagmaInstTraversableFreeAddMagma.proof_1 = (_ : LawfulFunctor FreeAddMagma)

ink

def FreeAddMagma.instIsLawfulTraversableFreeAddMagmaInstTraversableFreeAddMagma.proof_4 : ∀ {α β : Type u_1} (f : α → β) (x : FreeAddMagma α), traverse (pure ∘ f) x = id.mk (f <$> x)

Equations

• (_ : traverse (pure ∘ f) x = id.mk (f <$> x)) = (_ : traverse (pure ∘ f) x = id.mk (f <$> x))

ink

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.

ink

instance FreeMagma.instIsLawfulTraversableFreeMagmaInstTraversableFreeMagma : IsLawfulTraversable FreeMagma

Equations

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

ink

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

Representation of an element of a free magma.

Equations

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

ink

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

Representation of an element of a free additive magma.

Equations

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

ink

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

Equations

• instReprFreeAddMagma = { reprPrec := fun o x => FreeAddMagma.repr o }

ink

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

Equations

• instReprFreeMagma = { reprPrec := fun o x => FreeMagma.repr o }

ink

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

Length of an element of a free magma.

Equations

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

ink

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

Length of an element of a free additive magma.

Equations

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

ink

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

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

Associativity relations for an additive magma.

ink

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

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

Associativity relations for a magma.

ink

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

Additive semigroup quotient of an additive magma.

Equations

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

ink

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

Semigroup quotient of a magma.

Equations

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

ink

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

ink

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

ink

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

ink

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

ink

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.

ink

def AddMagma.FreeAddSemigroup.instAddSemigroupAssocQuotient.proof_3 {α : Type u_1} [inst : Add α] (x : AddMagma.FreeAddSemigroup α) (y : AddMagma.FreeAddSemigroup α) (z : AddMagma.FreeAddSemigroup α) : x + y + z = x + (y + z)

Equations

• (_ : x + y + z = x + (y + z)) = (_ : x + y + z = x + (y + z))

ink

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

Equations

• AddMagma.FreeAddSemigroup.instAddSemigroupAssocQuotient = AddSemigroup.mk (_ : ∀ (x y z : AddMagma.FreeAddSemigroup α), x + y + z = x + (y + z))

ink

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.

ink

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

Equations

• Magma.AssocQuotient.instSemigroupAssocQuotient = Semigroup.mk (_ : ∀ (x y z : Magma.AssocQuotient α), x * y * z = x * (y * z))

ink

def AddMagma.FreeAddSemigroup.of.proof_1 {α : Type u_1} [inst : Add α] (_x : α) (_y : α) : Quot.mk (AddMagma.AssocRel α) (_x + _y) = Quot.mk (AddMagma.AssocRel α) (_x + _y)

Equations

• (_ : Quot.mk (AddMagma.AssocRel α) (_x + _y) = Quot.mk (AddMagma.AssocRel α) (_x + _y)) = (_ : Quot.mk (AddMagma.AssocRel α) (_x + _y) = Quot.mk (AddMagma.AssocRel α) (_x + _y))

ink

def AddMagma.FreeAddSemigroup.of {α : Type u} [inst : Add α] : AddHom α (AddMagma.FreeAddSemigroup α)

Embedding from additive magma to its free additive semigroup.

Equations

• AddMagma.FreeAddSemigroup.of = { toFun := Quot.mk (AddMagma.AssocRel α), map_add' := (_ : ∀ (_x _y : α), Quot.mk (AddMagma.AssocRel α) (_x + _y) = Quot.mk (AddMagma.AssocRel α) (_x + _y)) }

ink

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

Embedding from magma to its free semigroup.

Equations

• Magma.AssocQuotient.of = { toFun := Quot.mk (Magma.AssocRel α), map_mul' := (_ : ∀ (_x _y : α), Quot.mk (Magma.AssocRel α) (_x * _y) = Quot.mk (Magma.AssocRel α) (_x * _y)) }

ink

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

Equations

• AddMagma.FreeAddSemigroup.instInhabitedAssocQuotient = { default := ↑AddMagma.FreeAddSemigroup.of default }

ink

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

Equations

• Magma.AssocQuotient.instInhabitedAssocQuotient = { default := ↑Magma.AssocQuotient.of default }

ink

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

ink

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

ink

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

ink

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

ink

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 b → ↑f a = ↑f b)) (x + y) = (fun x => Quot.liftOn x ↑f (_ : ∀ (a b : α), AddMagma.AssocRel α a b → ↑f a = ↑f b)) x + (fun x => Quot.liftOn x ↑f (_ : ∀ (a b : α), AddMagma.AssocRel α a b → ↑f a = ↑f b)) y

Equations

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

ink

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 b → ↑f a = ↑f b), map_add' := (_ : ∀ (x y : AddMagma.FreeAddSemigroup α), (fun x => Quot.liftOn x ↑f (_ : ∀ (a b : α), AddMagma.AssocRel α a b → ↑f a = ↑f b)) (x + y) = (fun x => Quot.liftOn x ↑f (_ : ∀ (a b : α), AddMagma.AssocRel α a b → ↑f a = ↑f b)) x + (fun x => Quot.liftOn x ↑f (_ : ∀ (a b : α), AddMagma.AssocRel α a b → ↑f 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.

ink

def AddMagma.FreeAddSemigroup.lift.proof_1 {α : Type u_1} [inst : Add α] {β : Type u_2} [inst : AddSemigroup β] (f : AddHom α β) (a : α) (b : α) : AddMagma.AssocRel α a b → ↑f a = ↑f b

Equations

• (_ : ↑f a = ↑f b) = (_ : ↑f a = ↑f b)

ink

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 b → ↑f a = ↑f b), map_add' := (_ : ∀ (x y : AddMagma.FreeAddSemigroup α), (fun x => Quot.liftOn x ↑f (_ : ∀ (a b : α), AddMagma.AssocRel α a b → ↑f a = ↑f b)) (x + y) = (fun x => Quot.liftOn x ↑f (_ : ∀ (a b : α), AddMagma.AssocRel α a b → ↑f a = ↑f b)) x + (fun x => Quot.liftOn x ↑f (_ : ∀ (a b : α), AddMagma.AssocRel α a b → ↑f a = ↑f b)) y) }) f) = f

Equations

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

ink

def AddMagma.FreeAddSemigroup.lift {α : Type u} [inst : Add α] {β : Type v} [inst : AddSemigroup β] : AddHom α β ≃ AddHom (AddMagma.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.

ink

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

ink

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

ink

def Magma.AssocQuotient.lift {α : Type u} [inst : Mul α] {β : Type v} [inst : Semigroup β] : (α →ₙ* β) ≃ (Magma.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.

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

def AddMagma.FreeAddSemigroup.map {α : Type u} [inst : Add α] {β : Type v} [inst : Add β] (f : AddHom α β) : AddHom (AddMagma.FreeAddSemigroup α) (AddMagma.FreeAddSemigroup β)

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

Equations

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

ink

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

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

Equations

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

ink

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

ink

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

ink

structure FreeAddSemigroup (α : Type u) : Type u

• The head of the element

  head : α

• The tail of the element

  tail : List α

Free additive semigroup over a given alphabet.

ink

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

ink

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

ink

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

ink

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

ink

structure FreeSemigroup (α : Type u) : Type u

• The head of the element

  head : α

• The tail of the element

  tail : List α

Free semigroup over a given alphabet.

ink

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

ink

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

Equations

• FreeAddSemigroup.instAddSemigroupFreeAddSemigroup = AddSemigroup.mk (_ : ∀ (_L1 _L2 _L3 : FreeAddSemigroup α), _L1 + _L2 + _L3 = _L1 + (_L2 + _L3))

ink

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

Equations

• FreeSemigroup.instSemigroupFreeSemigroup = Semigroup.mk (_ : ∀ (_L1 _L2 _L3 : FreeSemigroup α), _L1 * _L2 * _L3 = _L1 * (_L2 * _L3))

ink

@[simp]

theorem FreeAddSemigroup.head_add {α : Type u} (x : FreeAddSemigroup α) (y : FreeAddSemigroup α) : (x + y).head = x.head

ink

@[simp]

theorem FreeSemigroup.head_mul {α : Type u} (x : FreeSemigroup α) (y : FreeSemigroup α) : (x * y).head = x.head

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

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

The embedding α → free_add_semigroup α→ free_add_semigroup α.

Equations

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

theorem FreeSemigroup.of_tail {α : Type u} (x : α) : (FreeSemigroup.of x).tail = []

ink

@[simp]

theorem FreeAddSemigroup.of_tail {α : Type u} (x : α) : (FreeAddSemigroup.of x).tail = []

ink

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

The embedding α → FreeSemigroup α→ FreeSemigroup α.

Equations

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

ink

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

Length of an element of free additive semigroup

Equations

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

ink

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

Length of an element of free semigroup.

Equations

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

ink

@[simp]

theorem FreeAddSemigroup.length_add {α : Type u} (x : FreeAddSemigroup α) (y : FreeAddSemigroup α) : FreeAddSemigroup.length (x + y) = FreeAddSemigroup.length x + FreeAddSemigroup.length y

ink

@[simp]

theorem FreeSemigroup.length_mul {α : Type u} (x : FreeSemigroup α) (y : FreeSemigroup α) : FreeSemigroup.length (x * y) = FreeSemigroup.length x + FreeSemigroup.length y

ink

@[simp]

theorem FreeAddSemigroup.length_of {α : Type u} (x : α) : FreeAddSemigroup.length (FreeAddSemigroup.of x) = 1

ink

@[simp]

theorem FreeSemigroup.length_of {α : Type u} (x : α) : FreeSemigroup.length (FreeSemigroup.of x) = 1

ink

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

Equations

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

ink

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

Equations

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

ink

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 y → C (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.

ink

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 y → C (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.

ink

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

ink

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

ink

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.

ink

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.

ink

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.

ink

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.

ink

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

ink

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

ink

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.

ink

@[simp]

theorem FreeAddSemigroup.lift_of {α : Type u} {β : Type v} [inst : AddSemigroup β] (f : α → β) (x : α) : ↑(↑FreeAddSemigroup.lift f) (FreeAddSemigroup.of x) = f x

ink

@[simp]

theorem FreeSemigroup.lift_of {α : Type u} {β : Type v} [inst : Semigroup β] (f : α → β) (x : α) : ↑(↑FreeSemigroup.lift f) (FreeSemigroup.of x) = f x

ink

@[simp]

theorem FreeAddSemigroup.lift_comp_of {α : Type u} {β : Type v} [inst : AddSemigroup β] (f : α → β) : ↑(↑FreeAddSemigroup.lift f) ∘ FreeAddSemigroup.of = f

ink

@[simp]

theorem FreeSemigroup.lift_comp_of {α : Type u} {β : Type v} [inst : Semigroup β] (f : α → β) : ↑(↑FreeSemigroup.lift f) ∘ FreeSemigroup.of = f

ink

@[simp]

theorem FreeAddSemigroup.lift_comp_of' {α : Type u} {β : Type v} [inst : AddSemigroup β] (f : AddHom (FreeAddSemigroup α) β) : ↑FreeAddSemigroup.lift (↑f ∘ FreeAddSemigroup.of) = f

ink

@[simp]

theorem FreeSemigroup.lift_comp_of' {α : Type u} {β : Type v} [inst : Semigroup β] (f : FreeSemigroup α →ₙ* β) : ↑FreeSemigroup.lift (↑f ∘ FreeSemigroup.of) = f

ink

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

ink

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

ink

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

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

Equations

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

ink

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)

ink

@[simp]

theorem FreeAddSemigroup.map_of {α : Type u} {β : Type v} (f : α → β) (x : α) : ↑(FreeAddSemigroup.map f) (FreeAddSemigroup.of x) = FreeAddSemigroup.of (f x)

ink

@[simp]

theorem FreeSemigroup.map_of {α : Type u} {β : Type v} (f : α → β) (x : α) : ↑(FreeSemigroup.map f) (FreeSemigroup.of x) = FreeSemigroup.of (f x)

ink

@[simp]

theorem FreeAddSemigroup.length_map {α : Type u} {β : Type v} (f : α → β) (x : FreeAddSemigroup α) : FreeAddSemigroup.length (↑(FreeAddSemigroup.map f) x) = FreeAddSemigroup.length x

ink

@[simp]

theorem FreeSemigroup.length_map {α : Type u} {β : Type v} (f : α → β) (x : FreeSemigroup α) : FreeSemigroup.length (↑(FreeSemigroup.map f) x) = FreeSemigroup.length x

ink

instance FreeAddSemigroup.instMonadFreeAddSemigroup : Monad FreeAddSemigroup

Equations

• FreeAddSemigroup.instMonadFreeAddSemigroup = Monad.mk

ink

instance FreeSemigroup.instMonadFreeSemigroup : Monad FreeSemigroup

Equations

• FreeSemigroup.instMonadFreeSemigroup = Monad.mk

ink

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 y → C (pure x + y)) : C x

Recursor that uses pure instead of of.

Equations

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

ink

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

Recursor that uses pure instead of of.

Equations

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

ink

@[simp]

theorem FreeAddSemigroup.map_pure {α : Type u} {β : Type u} (f : α → β) (x : α) : f <$> pure x = pure (f x)

ink

@[simp]

theorem FreeSemigroup.map_pure {α : Type u} {β : Type u} (f : α → β) (x : α) : f <$> pure x = pure (f x)

ink

@[simp]

theorem FreeAddSemigroup.map_add' {α : Type u} {β : Type u} (f : α → β) (x : FreeAddSemigroup α) (y : FreeAddSemigroup α) : f <$> (x + y) = f <$> x + f <$> y

ink

@[simp]

theorem FreeSemigroup.map_mul' {α : Type u} {β : Type u} (f : α → β) (x : FreeSemigroup α) (y : FreeSemigroup α) : f <$> (x * y) = f <$> x * f <$> y

ink

@[simp]

theorem FreeAddSemigroup.pure_bind {α : Type u} {β : Type u} (f : α → FreeAddSemigroup β) (x : α) : pure x >>= f = f x

ink

@[simp]

theorem FreeSemigroup.pure_bind {α : Type u} {β : Type u} (f : α → FreeSemigroup β) (x : α) : pure x >>= f = f x

ink

@[simp]

theorem FreeAddSemigroup.add_bind {α : Type u} {β : Type u} (f : α → FreeAddSemigroup β) (x : FreeAddSemigroup α) (y : FreeAddSemigroup α) : x + y >>= f = (x >>= f) + (y >>= f)

ink

@[simp]

theorem FreeSemigroup.mul_bind {α : Type u} {β : Type u} (f : α → FreeSemigroup β) (x : FreeSemigroup α) (y : FreeSemigroup α) : x * y >>= f = (x >>= f) * (y >>= f)

ink

@[simp]

theorem FreeAddSemigroup.pure_seq {α : Type u} {β : Type u} {f : α → β} {x : FreeAddSemigroup α} : (Seq.seq (pure f) fun x => x) = f <$> x

ink

@[simp]

theorem FreeSemigroup.pure_seq {α : Type u} {β : Type u} {f : α → β} {x : FreeSemigroup α} : (Seq.seq (pure f) fun x => x) = f <$> x

ink

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

ink

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

ink

instance FreeAddSemigroup.instLawfulMonadFreeAddSemigroupInstMonadFreeAddSemigroup : LawfulMonad FreeAddSemigroup

Equations

• FreeAddSemigroup.instLawfulMonadFreeAddSemigroupInstMonadFreeAddSemigroup = FreeAddSemigroup.instLawfulMonadFreeAddSemigroupInstMonadFreeAddSemigroup.proof_1

ink

def FreeAddSemigroup.instLawfulMonadFreeAddSemigroupInstMonadFreeAddSemigroup.proof_1 : LawfulMonad FreeAddSemigroup

Equations

• FreeAddSemigroup.instLawfulMonadFreeAddSemigroupInstMonadFreeAddSemigroup.proof_1 = (_ : LawfulMonad FreeAddSemigroup)

ink

instance FreeSemigroup.instLawfulMonadFreeSemigroupInstMonadFreeSemigroup : LawfulMonad FreeSemigroup

Equations

• FreeSemigroup.instLawfulMonadFreeSemigroupInstMonadFreeSemigroup = FreeSemigroup.instLawfulMonadFreeSemigroupInstMonadFreeSemigroup.proof_1

ink

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

FreeAddSemigroup is traversable.

Equations

• FreeAddSemigroup.traverse F x = FreeAddSemigroup.recOnPure x (fun x => pure <$> F x) fun _x _y ihx ihy => Seq.seq ((fun x x_1 => x + x_1) <$> ihx) fun x => ihy

ink

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

FreeSemigroup is traversable.

Equations

• FreeSemigroup.traverse F x = FreeSemigroup.recOnPure x (fun x => pure <$> F x) fun _x _y ihx ihy => Seq.seq ((fun x x_1 => x * x_1) <$> ihx) fun x => ihy

ink

noncomputable instance FreeAddSemigroup.instTraversableFreeAddSemigroup : Traversable FreeAddSemigroup

Equations

• FreeAddSemigroup.instTraversableFreeAddSemigroup = Traversable.mk @FreeAddSemigroup.traverse

ink

noncomputable instance FreeSemigroup.instTraversableFreeSemigroup : Traversable FreeSemigroup

Equations

• FreeSemigroup.instTraversableFreeSemigroup = Traversable.mk @FreeSemigroup.traverse

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

noncomputable instance FreeAddSemigroup.instIsLawfulTraversableFreeAddSemigroupInstTraversableFreeAddSemigroup : IsLawfulTraversable FreeAddSemigroup

Equations

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

ink

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.

ink

def FreeAddSemigroup.instIsLawfulTraversableFreeAddSemigroupInstTraversableFreeAddSemigroup.proof_1 : LawfulFunctor FreeAddSemigroup

Equations

• FreeAddSemigroup.instIsLawfulTraversableFreeAddSemigroupInstTraversableFreeAddSemigroup.proof_1 = (_ : LawfulFunctor FreeAddSemigroup)

ink

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.

ink

def FreeAddSemigroup.instIsLawfulTraversableFreeAddSemigroupInstTraversableFreeAddSemigroup.proof_4 : ∀ {α β : Type u_1} (f : α → β) (x : FreeAddSemigroup α), traverse (pure ∘ f) x = id.mk (f <$> x)

Equations

• (_ : traverse (pure ∘ f) x = id.mk (f <$> x)) = (_ : traverse (pure ∘ f) x = id.mk (f <$> x))

ink

def FreeAddSemigroup.instIsLawfulTraversableFreeAddSemigroupInstTraversableFreeAddSemigroup.proof_2 : ∀ {α : Type u_1} (x : FreeAddSemigroup α), traverse pure x = x

Equations

• (_ : traverse pure x = x) = (_ : traverse pure x = x)

ink

noncomputable instance FreeSemigroup.instIsLawfulTraversableFreeSemigroupInstTraversableFreeSemigroup : IsLawfulTraversable FreeSemigroup

Equations

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

ink

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

Equations

• FreeAddSemigroup.instDecidableEqFreeAddSemigroup x x = decidable_of_iff' (x.head = x.head ∧ x.tail = x.tail) (_ : x = x ↔ x.head = x.head ∧ x.tail = x.tail)

ink

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

Equations

• FreeSemigroup.instDecidableEqFreeSemigroup x x = decidable_of_iff' (x.head = x.head ∧ x.tail = x.tail) (_ : x = x ↔ x.head = x.head ∧ x.tail = x.tail)

ink

def FreeAddMagma.toFreeAddSemigroup {α : Type u} : AddHom (FreeAddMagma α) (FreeAddSemigroup α)

The canonical additive morphism from FreeAddMagma α to FreeAddSemigroup α.

Equations

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

ink

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

The canonical multiplicative morphism from FreeMagma α to FreeSemigroup α.

Equations

• FreeMagma.toFreeSemigroup = ↑FreeMagma.lift FreeSemigroup.of

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

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.

ink

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.

ink

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

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

Equations

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

ink

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

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

Equations

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