---

Step * 2 2 1 1 1 1 of Lemma mul-ipoly-ringeq


1. r : CRng
2. p : iMonomial() List
3. q : iMonomial() List
⊢ ipolynomial-term(p) ≡ ipolynomial-term(p) (+) (ipolynomial-term([]) (*) ipolynomial-term(q))
BY
{ (GenConclTerms Auto [⌜ipolynomial-term(p)⌝;⌜ipolynomial-term(q)⌝]⋅ THEN All Thin) }

1
1. r : CRng
2. v : int_term()
3. v1 : int_term()
⊢ v ≡ v (+) (ipolynomial-term([]) (*) v1)

---

Latex:

---

Latex:

1.  r  :  CRng
2.  p  :  iMonomial()  List
3.  q  :  iMonomial()  List
\mvdash{}  ipolynomial-term(p)  \mequiv{}  ipolynomial-term(p)  (+)  (ipolynomial-term([])  (*)  ipolynomial-term(q))


By

---

Latex:
(GenConclTerms  Auto  [\mkleeneopen{}ipolynomial-term(p)\mkleeneclose{};\mkleeneopen{}ipolynomial-term(q)\mkleeneclose{}]\mcdot{}  THEN  All  Thin)

---

Home Index