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.

noncomputable def FirstOrder.Ring.termOfFreeCommRing {α : Type u_1} (p : FreeCommRing α) : FirstOrder.Language.Term FirstOrder.Language.ring α

Make a Language.ring.Term α from an element of FreeCommRing α

Equations

• FirstOrder.Ring.termOfFreeCommRing p = Classical.choose (_ : ∃ (t : FirstOrder.Language.Term FirstOrder.Language.ring α), FirstOrder.Language.Term.realize FreeCommRing.of t = p)

@[simp]

theorem FirstOrder.Ring.realize_termOfFreeCommRing {α : Type u_1} {R : Type u_2} [CommRing R] [FirstOrder.Ring.CompatibleRing R] (p : FreeCommRing α) (v : α → R) : FirstOrder.Language.Term.realize v (FirstOrder.Ring.termOfFreeCommRing p) = (FreeCommRing.lift v) p