Making a term in the language of rings from an element of the FreeCommRing #
This file defines the function FirstOrder.Ring.termOfFreeCommRing
which constructs a
Language.ring.Term α
from an element of FreeCommRing α
.
The theorem FirstOrder.Ring.realize_termOfFreeCommRing
shows that the term constructed when
realized in a ring R
is equal to the lift of the element of FreeCommRing α
to R
.
Make a Language.ring.Term α
from an element of FreeCommRing α