---

Step * 1 of Lemma ipolynomial-term-cons-ringeq


1. r : Rng
2. m : iMonomial()
⊢ imonomial-term(m) ≡ imonomial-term(m) (+) "0"
BY
{ (D 0 THEN Reduce 0 THEN Auto THEN RWO "int-to-ring-zero" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  r  :  Rng
2.  m  :  iMonomial()
\mvdash{}  imonomial-term(m)  \mequiv{}  imonomial-term(m)  (+)  "0"


By

---

Latex:
(D  0  THEN  Reduce  0  THEN  Auto  THEN  RWO  "int-to-ring-zero"  0  THEN  Auto)

---

Home Index