---

Step * 1 2 of Lemma ring_term_polynomial


1. r : CRng
2. const : ℤ
3. ¬(const = 0 ∈ ℤ)
⊢ ipolynomial-term([<const, []>]) ≡ "const"
BY
{ xxx(RepUR ``ipolynomial-term imonomial-term`` 0 THEN ((D 0 THEN Auto) THEN RepUR ``int_term_value`` 0) THEN Auto)xxx }

---

Latex:

---

Latex:

1.  r  :  CRng
2.  const  :  \mBbbZ{}
3.  \mneg{}(const  =  0)
\mvdash{}  ipolynomial-term([<const,  []>])  \mequiv{}  "const"


By

---

Latex:
xxx(RepUR  ``ipolynomial-term  imonomial-term``  0
        THEN  ((D  0  THEN  Auto)  THEN  RepUR  ``int\_term\_value``  0)
        THEN  Auto)xxx

---

Home Index