Lean4
/-- If `α` is a type, then `FreeRing α` is the free ring generated by `α`.
This is a ring equipped with a function `FreeRing.of : α → FreeRing α` which has
the following universal property: if `R` is any ring, and `f : α → R` is any function,
then this function is the composite of `FreeRing.of` and a unique ring homomorphism
`FreeRing.lift f : FreeRing α →+* R`.
A typical element of `FreeRing α` is a `ℤ`-linear combination of
formal products of elements of `α`.
For example if `x` and `y` are terms of type `α` then `3 * x * y * x - 2 * y * x + 1` is a
"typical" element of `FreeRing α`. In particular if `α` is empty
then `FreeRing α` is isomorphic to `ℤ`, and if `α` has one term `t`
then `FreeRing α` is isomorphic to the polynomial ring `ℤ[t]`.
If `α` has two or more terms then `FreeRing α` is not commutative.
One can think of `FreeRing α` as the free non-commutative polynomial ring
with coefficients in the integers and variables indexed by `α`.
-/
def FreeRing (α : Type u) : Type u :=
FreeAbelianGroup <| FreeMonoid α
