---

Step * 1 of Lemma int_mod_ring_wf


1. n : ℕ+
⊢ int_mod_ring(n) ∈ CDRng
BY
{ (Unfold `int_mod_ring` 0 THEN MemTypeCD THEN Reduce 0) }

1
1. n : ℕ+
⊢ <ℤ_n, λu,v. (u mod n =z v mod n), λu,v. ff, λu,v. (u + v), 0, λu.(-u), λu,v. (u * v), 1, λu,v. (inr ⋅ )> ∈ CRng

2
1. n : ℕ+
⊢ IsEqFun(ℤ_n;λu,v. (u mod n =z v mod n))

3
.....wf..... 
1. n : ℕ+
2. r : CRng
⊢ istype(IsEqFun(|r|;=b))

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
\mvdash{}  int\_mod\_ring(n)  \mmember{}  CDRng


By

---

Latex:
(Unfold  `int\_mod\_ring`  0  THEN  MemTypeCD  THEN  Reduce  0)

---

Home Index