---

Step * of Lemma imonomial-term-linear-ringeq

∀r:Rng. ∀f:ℤ ⟶ |r|. ∀ws:ℤ List. ∀c:ℤ.  (ring_term_value(f;imonomial-term(<c, ws>)) = (int-to-ring(r;c) * ring_term_valu\000Ce(f;imonomial-term(<1, ws>))) ∈ |r|)
BY
{ xxx((Auto THEN Unfold `imonomial-term` 0)
      THEN Reduce 0
      THEN (RW  (AddrC [2] (LemmaC `imonomial-ringeq-lemma`)) 0 THENA Auto)
      THEN Reduce 0
      THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}r:Rng.  \mforall{}f:\mBbbZ{}  {}\mrightarrow{}  |r|.  \mforall{}ws:\mBbbZ{}  List.  \mforall{}c:\mBbbZ{}.
    (ring\_term\_value(f;imonomial-term(<c,  ws>))  =  (int-to-ring(r;c)  *  ring\_term\_value(f;imonomial-term\000C(ə,  ws>))))


By

---

Latex:
xxx((Auto  THEN  Unfold  `imonomial-term`  0)
        THEN  Reduce  0
        THEN  (RW    (AddrC  [2]  (LemmaC  `imonomial-ringeq-lemma`))  0  THENA  Auto)
        THEN  Reduce  0
        THEN  Auto)xxx

---

Home Index