Lean4
/-- If `α` is a type, then `FreeAbelianGroup α` is the free abelian group generated by `α`.
This is an abelian group equipped with a function
`FreeAbelianGroup.of : α → FreeAbelianGroup α` which has the following universal property:
if `G` is any abelian group, and `f : α → G` is any function, then this function is
the composite of `FreeAbelianGroup.of` and a unique group homomorphism
`FreeAbelianGroup.lift f : FreeAbelianGroup α →+ G`.
A typical element of `FreeAbelianGroup α` is a formal sum of
elements of `α` and their formal inverses.
For example if `x` and `y` are terms of type `α` then `x + x + x - y` is a
"typical" element of `FreeAbelianGroup α`. In particular if `α` is empty
then `FreeAbelianGroup α` is isomorphic to the trivial group, and if `α` has one term
then `FreeAbelianGroup α` is isomorphic to `ℤ`.
One can think of `FreeAbelianGroup α` as the functions `α →₀ ℤ` with finite support,
and addition given pointwise.
TODO: rename to `FreeAddCommGroup` and introduce a multiplicative version
-/
def FreeAbelianGroup : Type u :=
Additive <| Abelianization <| FreeGroup α
