---

Step * 1 of Lemma lookup_omral_times

.....assertion..... 
1. g : OCMon
2. r : CDRng
3. qs : |omral(g;r)|
4. z : |g|
⊢ ∀r:CDRng. (r↓+gp ∈ IAbMonoid)
BY
{ (InstLemma `cdrng_is_abdmonoid` []⋅ THEN ParallelLast THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
1.  g  :  OCMon
2.  r  :  CDRng
3.  qs  :  |omral(g;r)|
4.  z  :  |g|
\mvdash{}  \mforall{}r:CDRng.  (r\mdownarrow{}+gp  \mmember{}  IAbMonoid)


By

---

Latex:
(InstLemma  `cdrng\_is\_abdmonoid`  []\mcdot{}  THEN  ParallelLast  THEN  Auto)

---

Home Index