---

Step * 1 of Lemma ring_polynomial_null


1. r : CRng
2. t : int_term()
3. ipolynomial-term([]) ≡ t
4. inl Ax ≤ tt
⊢ t ≡ "0"
BY
{ (RepUR ``ipolynomial-term`` -2 THEN RepeatFor 2 (ParallelOp -2) THEN Auto) }

---

Latex:

---

Latex:

1.  r  :  CRng
2.  t  :  int\_term()
3.  ipolynomial-term([])  \mequiv{}  t
4.  inl  Ax  \mleq{}  tt
\mvdash{}  t  \mequiv{}  "0"


By

---

Latex:
(RepUR  ``ipolynomial-term``  -2  THEN  RepeatFor  2  (ParallelOp  -2)  THEN  Auto)

---

Home Index