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