Lean4
/-- If `α` is a type, then `FreeMonoid α` is the free monoid generated by `α`.
This is a monoid equipped with a function `FreeMonoid.of : α → FreeMonoid α` which has
the following universal property: if `M` is any monoid, and `f : α → M` is any function,
then this function is the composite of `FreeMonoid.of` and a unique monoid homomorphism
`FreeMonoid.lift f : FreeMonoid α →* M`.
A typical element of `FreeMonoid α` is a 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 `FreeMonoid α`. In particular if `α` is empty
then `FreeMonoid α` is isomorphic to the trivial monoid, and if `α` has one term
then `FreeMonoid α` is isomorphic to `Multiplicative ℕ`.
If `α` has two or more terms then `FreeMonoid α` is not commutative.
One can think of `FreeMonoid α` as the type of lists of `α`, with multiplication
given by concatenation.
-/
@[to_additive /-- If `α` is a type, then `FreeAddMonoid α` is the free additive monoid generated by `α`.
This is a monoid equipped with a function `FreeAddMonoid.of : α → FreeAddMonoid α` which has
the following universal property: if `M` is any monoid, and `f : α → M` is any function,
then this function is the composite of `FreeAddMonoid.of` and a unique monoid homomorphism
`FreeAddMonoid.lift f : FreeAddMonoid α →+ M`.
A typical element of `FreeAddMonoid α` is a 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 `FreeAddMonoid α`. In particular if `α` is empty
then `FreeAddMonoid α` is isomorphic to the trivial monoid, and if `α` has one term
then `FreeAddMonoid α` is isomorphic to `ℕ`.
If `α` has two or more terms then `FreeAddMonoid α` is not commutative.
One can think of `FreeAddMonoid α` as the type of lists of `α`, with addition
given by concatenation. -/
]
def FreeMonoid (α) :=
List α
