---

Step * 2 of Lemma rat_term_polynomial


1. var : ℤ
⊢ rtermVar(var) ≡ ipolynomial-term([<1, [var]>])/ipolynomial-term([<1, []>])
BY
{ (RepUR ``ipolynomial-term imonomial-term req_rat_term`` 0 THEN Auto THEN nRMul ⌜r1⌝ 0⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  var  :  \mBbbZ{}
\mvdash{}  rtermVar(var)  \mequiv{}  ipolynomial-term([ə,  [var]>])/ipolynomial-term([ə,  []>])


By

---

Latex:
(RepUR  ``ipolynomial-term  imonomial-term  req\_rat\_term``  0  THEN  Auto  THEN  nRMul  \mkleeneopen{}r1\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index