Theorems · Definition · group theory

FreeAddMonoid

Type u_6 → Type u_6

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.

Defined in

Mathlib.Algebra.FreeMonoid.Basic

Cited by

145 results in Mathlib

Foundations

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