---

Step * of Lemma int_ring_wf

ℤ-rng ∈ IntegDom{i}
BY
{ MemTypeCD⋅ }

1
ℤ-rng ∈ CRng

2
.....set predicate..... 
IsIntegDom(ℤ-rng)

3
.....wf..... 
1. r : CRng
⊢ IsIntegDom(r) ∈ Type

---

Latex:

---

Latex:
\mBbbZ{}-rng  \mmember{}  IntegDom\{i\}


By

---

Latex:
MemTypeCD\mcdot{}

---

Home Index