Documentation

Mathlib.ModelTheory.Algebra.Ring.FreeCommRing

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 α

Equations
Instances For