---

Step * 1 2 of Lemma int_ring_wf

.....set predicate..... 
Comm(|ℤ-rng|;*)
BY
{ AbEval ``comm`` 0 
THEN Auto }

---

Latex:

---

Latex:
.....set  predicate..... 
Comm(|\mBbbZ{}-rng|;*)


By

---

Latex:
AbEval  ``comm``  0 
THEN  Auto

---

Home Index