---

Step * 1 1 1 of Lemma mul-monomials-ringeq


1. r : CRng
2. f : ℤ ⟶ |r|
⊢ ∀as:ℤ List. (ring_term_value(f;imonomial-term(<1, merge-int(as;[])>)) = (ring_term_value(f;imonomial-term(<1, as>)) * \000Cring_term_value(f;imonomial-term(<1, []>))) ∈ |r|)
BY
{ ((Unfold `merge-int` 0 THEN Reduce  0 THEN Auto)
   THEN RepUR ``imonomial-term`` 0
   THEN Auto
   THEN RWO "int-to-ring-one" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  r  :  CRng
2.  f  :  \mBbbZ{}  {}\mrightarrow{}  |r|
\mvdash{}  \mforall{}as:\mBbbZ{}  List.  (ring\_term\_value(f;imonomial-term(ə,  merge-int(as;[])>))  =  (ring\_term\_value(f;imonomi\000Cal-term(ə,  as>))  *  ring\_term\_value(f;imonomial-term(ə,  []>))))


By

---

Latex:
((Unfold  `merge-int`  0  THEN  Reduce    0  THEN  Auto)
  THEN  RepUR  ``imonomial-term``  0
  THEN  Auto
  THEN  RWO  "int-to-ring-one"  0
  THEN  Auto)

---

Home Index