Theorems · Definition · group theory

FreeAddGroup

Type u → Type u

If α is a type, then FreeAddGroup α is the free additive group generated by α. This is a group equipped with a function FreeAddGroup.of : α → FreeAddGroup α which has the following universal property: if G is any group, and f : α → G is any function, then this function is the composite of FreeAddGroup.of and a unique group homomorphism FreeAddGroup.lift f : FreeAddGroup α →+ G. A typical element of FreeAddGroup α is a formal sum of elements of α and their formal inverses, quotient by reduction. For example if x and y are terms of type α then -x + y + y + x + -y is a "typical" element of FreeAddGroup α. In particular if α is empty then FreeAddGroup α is isomorphic to the trivial group, and if α has one term then FreeAddGroup α is isomorphic to ℤ. If α has two or more terms then FreeAddGroup α is not commutative. [Wikidata Q431078](https://www.wikidata.org/wiki/Q431078)

Defined in

Mathlib.GroupTheory.FreeGroup.Basic

Cited by

90 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms