---

Step * 5 of Lemma ring_term_polynomial


1. r : CRng
2. left : int_term()
3. right : int_term()
4. ipolynomial-term(int_term_to_ipoly(left)) ≡ left
5. ipolynomial-term(int_term_to_ipoly(right)) ≡ right
⊢ ipolynomial-term(mul_ipoly(int_term_to_ipoly(left);int_term_to_ipoly(right))) ≡ left (*) right
BY
{ xxx((InstLemma `mul-ipoly-ringeq` [⌜r⌝]⋅ THENA Auto)
      THEN (RWW "mul_poly-sq -1 -2 -3" 0 THENA Auto)
      THEN RelRST
      THEN Auto)xxx }

---

Latex:

---

Latex:

1.  r  :  CRng
2.  left  :  int\_term()
3.  right  :  int\_term()
4.  ipolynomial-term(int\_term\_to\_ipoly(left))  \mequiv{}  left
5.  ipolynomial-term(int\_term\_to\_ipoly(right))  \mequiv{}  right
\mvdash{}  ipolynomial-term(mul\_ipoly(int\_term\_to\_ipoly(left);int\_term\_to\_ipoly(right)))  \mequiv{}  left  (*)  right


By

---

Latex:
xxx((InstLemma  `mul-ipoly-ringeq`  [\mkleeneopen{}r\mkleeneclose{}]\mcdot{}  THENA  Auto)
        THEN  (RWW  "mul\_poly-sq  -1  -2  -3"  0  THENA  Auto)
        THEN  RelRST
        THEN  Auto)xxx

---

Home Index