---

Step * 1 1 2 of Lemma int_ring_wf

.....set predicate..... 
IsRing(|ℤ-rng|;+ℤ-rng;0;-ℤ-rng;*;1)
BY
{ AbEval ``ring_p eqfun_p group_p monoid_p bilinear assoc ident inverse`` 0 
THEN Auto
THEN All (RW assert_pushdownC)
THEN Auto }

---

Latex:

---

Latex:
.....set  predicate..... 
IsRing(|\mBbbZ{}-rng|;+\mBbbZ{}-rng;0;-\mBbbZ{}-rng;*;1)


By

---

Latex:
AbEval  ``ring\_p  eqfun\_p  group\_p  monoid\_p  bilinear  assoc  ident  inverse``  0 
THEN  Auto
THEN  All  (RW  assert\_pushdownC)
THEN  Auto

---

Home Index