Theorems · Definition · group theory

FreeMonoid

Type u_6 → Type u_6

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.

Defined in

Mathlib.Algebra.FreeMonoid.Basic

Cited by

147 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms